Theorem rabxm

Description: Law of excluded middle, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011)

	Ref	Expression
Assertion	rabxm	$$⊢A=\left\{x\in A|\phi \right\}\cup \left\{x\in A|\neg \phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		rabid2im	$$⊢\forall x\in A\left(\phi \vee \neg \phi \right)\to A=\left\{x\in A|\left(\phi \vee \neg \phi \right)\right\}$$
2		exmidd	$$⊢x\in A\to \left(\phi \vee \neg \phi \right)$$
3	1 2	mprg	$$⊢A=\left\{x\in A|\left(\phi \vee \neg \phi \right)\right\}$$
4		unrab	$$⊢\left\{x\in A|\phi \right\}\cup \left\{x\in A|\neg \phi \right\}=\left\{x\in A|\left(\phi \vee \neg \phi \right)\right\}$$
5	3 4	eqtr4i	$$⊢A=\left\{x\in A|\phi \right\}\cup \left\{x\in A|\neg \phi \right\}$$