axprALT

Description: Alternate proof of axpr . (Contributed by NM, 14-Nov-2006) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	axprALT	$⊢ \exists z \forall w ((w = x \lor w = y) \to w \in z)$

Step	Hyp	Ref	Expression
1		zfpair	$⊢ \{x, y\} \in V$
2	1	isseti	$⊢ \exists z z = \{x, y\}$
3		dfcleq	$⊢ z = \{x, y\} \leftrightarrow \forall w (w \in z \leftrightarrow w \in \{x, y\})$
4		vex	$⊢ w \in V$
5	4	elpr	$⊢ w \in \{x, y\} \leftrightarrow (w = x \lor w = y)$
6	5	bibi2i	$⊢ (w \in z \leftrightarrow w \in \{x, y\}) \leftrightarrow (w \in z \leftrightarrow (w = x \lor w = y))$
7		biimpr	$⊢ (w \in z \leftrightarrow (w = x \lor w = y)) \to ((w = x \lor w = y) \to w \in z)$
8	6 7	sylbi	$⊢ (w \in z \leftrightarrow w \in \{x, y\}) \to ((w = x \lor w = y) \to w \in z)$
9	8	alimi	$⊢ \forall w (w \in z \leftrightarrow w \in \{x, y\}) \to \forall w ((w = x \lor w = y) \to w \in z)$
10	3 9	sylbi	$⊢ z = \{x, y\} \to \forall w ((w = x \lor w = y) \to w \in z)$
11	2 10	eximii	$⊢ \exists z \forall w ((w = x \lor w = y) \to w \in z)$

Metamath Proof Explorer