Theorem prexg 4166

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 3665, prprc1 3663, and prprc2 3664. (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 3633	. . . . . 6 |- ( y = B -> { x , y } = { x , B } )
2	1	eleq1d 2223	. . . . 5 |- ( y = B -> ( { x , y } e. _V <-> { x , B } e. _V ) )
3		zfpair2 4165	. . . . 5 |- { x , y } e. _V
4	2, 3	vtoclg 2769	. . . 4 |- ( B e. W -> { x , B } e. _V )
5		preq1 3632	. . . . 5 |- ( x = A -> { x , B } = { A , B } )
6	5	eleq1d 2223	. . . 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 2780	. 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 1332   e. wcel 2125   _Vcvv 2709   {cpr 3557

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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-14 2128  ax-ext 2136  ax-sep 4078  ax-pr 4164

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-v 2711  df-un 3102  df-sn 3562  df-pr 3563

This theorem is referenced by:  prelpwi  4169  opexg  4183  opi2  4188  opth  4192  opeqsn  4207  opeqpr  4208  uniop  4210  unex  4395  tpexg  4398  op1stb  4432  op1stbg  4433  onun2  4443  opthreg  4509  relop  4729  acexmidlemv  5812  pr2ne  7106  exmidonfinlem  7107  exmidaclem  7122  sup3exmid  8807  xrex  9738  2strbasg  12230  2stropg  12231  isomninnlem  13542  trilpolemlt1  13553  iswomninnlem  13561  iswomni0  13563  ismkvnnlem  13564