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	|- { x , y } e. _V

Proof

Step	Hyp	Ref	Expression
1		ax-pr	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )
2	1	sepexi	|- E. z A. w ( w e. z <-> ( w = x \/ w = y ) )
3		dfcleq	|- ( z = { x , y } <-> A. w ( w e. z <-> w e. { x , y } ) )
4		vex	|- w e. _V
5	4	elpr	|- ( w e. { x , y } <-> ( w = x \/ w = y ) )
6	5	bibi2i	|- ( ( w e. z <-> w e. { x , y } ) <-> ( w e. z <-> ( w = x \/ w = y ) ) )
7	6	albii	|- ( A. w ( w e. z <-> w e. { x , y } ) <-> A. w ( w e. z <-> ( w = x \/ w = y ) ) )
8	3 7	bitri	|- ( z = { x , y } <-> A. w ( w e. z <-> ( w = x \/ w = y ) ) )
9	8	exbii	|- ( E. z z = { x , y } <-> E. z A. w ( w e. z <-> ( w = x \/ w = y ) ) )
10	2 9	mpbir	|- E. z z = { x , y }
11	10	issetri	|- { x , y } e. _V