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 = ( { x e. A | ph } u. { x e. A | -. ph } )

Proof

Step	Hyp	Ref	Expression
1		rabid2	|- ( A = { x e. A | ( ph \/ -. ph ) } <-> A. x e. A ( ph \/ -. ph ) )
2		exmidd	|- ( x e. A -> ( ph \/ -. ph ) )
3	1 2	mprgbir	|- A = { x e. A | ( ph \/ -. ph ) }
4		unrab	|- ( { x e. A | ph } u. { x e. A | -. ph } ) = { x e. A | ( ph \/ -. ph ) }
5	3 4	eqtr4i	|- A = ( { x e. A | ph } u. { x e. A | -. ph } )