Theorem prexg 4255

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 3743, prprc1 3741, and prprc2 3742. (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 3711	. . . . . 6 |- ( y = B -> { x , y } = { x , B } )
2	1	eleq1d 2274	. . . . 5 |- ( y = B -> ( { x , y } e. _V <-> { x , B } e. _V ) )
3		zfpair2 4254	. . . . 5 |- { x , y } e. _V
4	2, 3	vtoclg 2833	. . . 4 |- ( B e. W -> { x , B } e. _V )
5		preq1 3710	. . . . 5 |- ( x = A -> { x , B } = { A , B } )
6	5	eleq1d 2274	. . . 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 2844	. 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 1373   e. wcel 2176   _Vcvv 2772   {cpr 3634

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4162  ax-pr 4253

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640

This theorem is referenced by:  prelpwi  4258  opexg  4272  opi2  4277  opth  4281  opeqsn  4297  opeqpr  4298  uniop  4300  unex  4488  tpexg  4491  op1stb  4525  op1stbg  4526  onun2  4538  opthreg  4604  relop  4828  acexmidlemv  5942  en2prd  6909  pw2f1odclem  6931  pr2ne  7300  exmidonfinlem  7301  exmidaclem  7320  sup3exmid  9030  xrex  9978  2strbasg  12952  2stropg  12953  prdsex  13101  prdsval  13105  xpsfval  13180  xpsval  13184  gsumprval  13231  struct2slots2dom  15635  structiedg0val  15637  edgstruct  15656  isomninnlem  15969  trilpolemlt1  15980  iswomninnlem  15988  iswomni0  15990  ismkvnnlem  15991