Theorem prex

Description: The Axiom of Pairing using class variables. Theorem 7.13 of Quine p. 51. By virtue of its definition, an unordered pair remains a set (even though no longer a pair) even when its components are proper classes (see prprc ), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993)

	Ref	Expression
Assertion	prex	|- { A , B } e. _V

Proof

Step	Hyp	Ref	Expression
1		preq2	|- ( y = B -> { x , y } = { x , B } )
2	1	eleq1d	|- ( y = B -> ( { x , y } e. _V <-> { x , B } e. _V ) )
3		zfpair2	|- { x , y } e. _V
4	2 3	vtoclg	|- ( B e. _V -> { x , B } e. _V )
5		preq1	|- ( x = A -> { x , B } = { A , B } )
6	5	eleq1d	|- ( x = A -> ( { x , B } e. _V <-> { A , B } e. _V ) )
7	4 6	imbitrid	|- ( x = A -> ( B e. _V -> { A , B } e. _V ) )
8	7	vtocleg	|- ( A e. _V -> ( B e. _V -> { A , B } e. _V ) )
9		prprc1	|- ( -. A e. _V -> { A , B } = { B } )
10		snex	|- { B } e. _V
11	9 10	eqeltrdi	|- ( -. A e. _V -> { A , B } e. _V )
12		prprc2	|- ( -. B e. _V -> { A , B } = { A } )
13		snex	|- { A } e. _V
14	12 13	eqeltrdi	|- ( -. B e. _V -> { A , B } e. _V )
15	8 11 14	pm2.61nii	|- { A , B } e. _V