Theorem rabxm

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

	Ref	Expression
Assertion	rabxm	⊢ 𝐴 = ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∪ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } )

Proof

Step	Hyp	Ref	Expression
1		rabid2im	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∨ ¬ 𝜑 ) → 𝐴 = { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∨ ¬ 𝜑 ) } )
2		exmidd	⊢ ( 𝑥 ∈ 𝐴 → ( 𝜑 ∨ ¬ 𝜑 ) )
3	1 2	mprg	⊢ 𝐴 = { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∨ ¬ 𝜑 ) }
4		unrab	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∪ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ) = { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∨ ¬ 𝜑 ) }
5	3 4	eqtr4i	⊢ 𝐴 = ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∪ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } )