Theorem prexg 4295

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 3777, prprc1 3775, and prprc2 3776. (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 3744	. . . . . 6 |- ( y = B -> { x , y } = { x , B } )
2	1	eleq1d 2298	. . . . 5 |- ( y = B -> ( { x , y } e. _V <-> { x , B } e. _V ) )
3		zfpair2 4294	. . . . 5 |- { x , y } e. _V
4	2, 3	vtoclg 2861	. . . 4 |- ( B e. W -> { x , B } e. _V )
5		preq1 3743	. . . . 5 |- ( x = A -> { x , B } = { A , B } )
6	5	eleq1d 2298	. . . 4 |- ( x = A -> ( { x , B } e. _V <-> { A , B } e. _V ) )
7	4, 6	imbitrid 154	. . 3 |- ( x = A -> ( B e. W -> { A , B } e. _V ) )
8	7	vtocleg 2874	. 2 |- ( A e. V -> ( B e. W -> { A , B } e. _V ) )
9	8	imp 124	1 |- ( ( A e. V /\ B e. W ) -> { A , B } e. _V )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1395   e. wcel 2200   _Vcvv 2799   {cpr 3667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pr 4293

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673

This theorem is referenced by:  prelpw  4299  prelpwi  4300  opexg  4314  opi2  4319  opth  4323  opeqsn  4339  opeqpr  4340  uniop  4342  unex  4532  tpexg  4535  op1stb  4569  op1stbg  4570  onun2  4582  opthreg  4648  relop  4872  acexmidlemv  6005  2oex  6585  en2prd  6978  pw2f1odclem  7003  pr2ne  7376  exmidonfinlem  7382  exmidaclem  7401  sup3exmid  9115  xrex  10064  2strbasg  13168  2stropg  13169  prdsex  13317  prdsval  13321  xpsfval  13396  xpsval  13400  gsumprval  13447  struct2slots2dom  15854  structiedg0val  15856  edgstruct  15879  umgrbien  15925  upgr1edc  15936  upgr1eopdc  15938  isomninnlem  16458  trilpolemlt1  16469  iswomninnlem  16477  iswomni0  16479  ismkvnnlem  16480