Theorem 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\left(\left(w=x\vee w=y\right)\to w\in z\right)$$

Proof

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