This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \in A \| φ\} \cup \{x \in A \| \neg φ\}$

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