Theorem zfpair2

Description: Derive the abbreviated version of the Axiom of Pairing from ax-pr . See zfpair for its derivation from the other axioms. (Contributed by NM, 14-Nov-2006)

	Ref	Expression
Assertion	zfpair2	$$⊢\left\{x,y\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ax-pr	$$⊢\exists z\forall w\left(\left(w=x\vee w=y\right)\to w\in z\right)$$
2	1	bm1.3ii	$$⊢\exists z\forall w\left(w\in z\leftrightarrow \left(w=x\vee w=y\right)\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	6	albii	$$⊢\forall w\left(w\in z\leftrightarrow w\in \left\{x,y\right\}\right)\leftrightarrow \forall w\left(w\in z\leftrightarrow \left(w=x\vee w=y\right)\right)$$
8	3 7	bitri	$$⊢z=\left\{x,y\right\}\leftrightarrow \forall w\left(w\in z\leftrightarrow \left(w=x\vee w=y\right)\right)$$
9	8	exbii	$$⊢\exists zz=\left\{x,y\right\}\leftrightarrow \exists z\forall w\left(w\in z\leftrightarrow \left(w=x\vee w=y\right)\right)$$
10	2 9	mpbir	$$⊢\exists zz=\left\{x,y\right\}$$
11	10	issetri	$$⊢\left\{x,y\right\}\in \mathrm{V}$$