Theorem prexg 4133

Description: The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51, but restricted to classes which exist. For proper classes, see prprc 3633, prprc1 3631, and prprc2 3632. (Contributed by Jim Kingdon, 16-Sep-2018.)

Assertion

Ref	Expression
prexg	|- ( ( A e. V /\ B e. W ) -> { A , B } e. _V )

Proof of Theorem prexg

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		preq2 3601	. . . . . 6 |- ( y = B -> { x , y } = { x , B } )
2	1	eleq1d 2208	. . . . 5 |- ( y = B -> ( { x , y } e. _V <-> { x , B } e. _V ) )
3		zfpair2 4132	. . . . 5 |- { x , y } e. _V
4	2, 3	vtoclg 2746	. . . 4 |- ( B e. W -> { x , B } e. _V )
5		preq1 3600	. . . . 5 |- ( x = A -> { x , B } = { A , B } )
6	5	eleq1d 2208	. . . 4 |- ( x = A -> ( { x , B } e. _V <-> { A , B } e. _V ) )
7	4, 6	syl5ib 153	. . 3 |- ( x = A -> ( B e. W -> { A , B } e. _V ) )
8	7	vtocleg 2757	. 2 |- ( A e. V -> ( B e. W -> { A , B } e. _V ) )
9	8	imp 123	1 |- ( ( A e. V /\ B e. W ) -> { A , B } e. _V )

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1331   e. wcel 1480   _Vcvv 2686   {cpr 3528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-pr 4131

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534

This theorem is referenced by:  prelpwi  4136  opexg  4150  opi2  4155  opth  4159  opeqsn  4174  opeqpr  4175  uniop  4177  unex  4362  tpexg  4365  op1stb  4399  op1stbg  4400  onun2  4406  opthreg  4471  relop  4689  acexmidlemv  5772  pr2ne  7048  exmidonfinlem  7049  exmidaclem  7064  sup3exmid  8722  xrex  9646  2strbasg  12070  2stropg  12071  isomninnlem  13235  trilpolemlt1  13244