Theorem prexg 4245

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 3733, prprc1 3731, and prprc2 3732. (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 3701	. . . . . 6 |- ( y = B -> { x , y } = { x , B } )
2	1	eleq1d 2265	. . . . 5 |- ( y = B -> ( { x , y } e. _V <-> { x , B } e. _V ) )
3		zfpair2 4244	. . . . 5 |- { x , y } e. _V
4	2, 3	vtoclg 2824	. . . 4 |- ( B e. W -> { x , B } e. _V )
5		preq1 3700	. . . . 5 |- ( x = A -> { x , B } = { A , B } )
6	5	eleq1d 2265	. . . 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 2835	. 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 1364   e. wcel 2167   _Vcvv 2763   {cpr 3624

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-14 2170  ax-ext 2178  ax-sep 4152  ax-pr 4243

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630

This theorem is referenced by:  prelpwi  4248  opexg  4262  opi2  4267  opth  4271  opeqsn  4286  opeqpr  4287  uniop  4289  unex  4477  tpexg  4480  op1stb  4514  op1stbg  4515  onun2  4527  opthreg  4593  relop  4817  acexmidlemv  5923  pw2f1odclem  6904  pr2ne  7271  exmidonfinlem  7272  exmidaclem  7291  sup3exmid  9001  xrex  9948  2strbasg  12822  2stropg  12823  prdsex  12971  prdsval  12975  xpsfval  13050  xpsval  13054  gsumprval  13101  isomninnlem  15761  trilpolemlt1  15772  iswomninnlem  15780  iswomni0  15782  ismkvnnlem  15783