Theorem prexg 4299

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 3780, prprc1 3778, and prprc2 3779. (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 3747	. . . . . 6 |- ( y = B -> { x , y } = { x , B } )
2	1	eleq1d 2298	. . . . 5 |- ( y = B -> ( { x , y } e. _V <-> { x , B } e. _V ) )
3		zfpair2 4298	. . . . 5 |- { x , y } e. _V
4	2, 3	vtoclg 2862	. . . 4 |- ( B e. W -> { x , B } e. _V )
5		preq1 3746	. . . . 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 2875	. 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 2800   {cpr 3668

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 4205  ax-pr 4297

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 2802  df-un 3202  df-sn 3673  df-pr 3674

This theorem is referenced by:  prelpw  4303  prelpwi  4304  opexg  4318  opi2  4323  opth  4327  opeqsn  4343  opeqpr  4344  uniop  4346  unex  4536  tpexg  4539  op1stb  4573  op1stbg  4574  onun2  4586  opthreg  4652  relop  4878  acexmidlemv  6011  2oex  6594  en2prd  6987  pw2f1odclem  7015  pr2ne  7388  exmidonfinlem  7394  exmidaclem  7413  sup3exmid  9127  xrex  10081  2strbasg  13193  2stropg  13194  prdsex  13342  prdsval  13346  xpsfval  13421  xpsval  13425  gsumprval  13472  struct2slots2dom  15879  structiedg0val  15881  edgstruct  15905  umgrbien  15951  upgr1edc  15962  upgr1eopdc  15964  uspgr1edc  16079  usgr1e  16080  uspgr1eopdc  16082  uspgr1ewopdc  16083  usgr1eop  16084  usgr2v1e2w  16085  isomninnlem  16570  trilpolemlt1  16581  iswomninnlem  16589  iswomni0  16591  ismkvnnlem  16592