Theorem prexg 4189

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 3686, prprc1 3684, and prprc2 3685. (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 3654	. . . . . 6 |- ( y = B -> { x , y } = { x , B } )
2	1	eleq1d 2235	. . . . 5 |- ( y = B -> ( { x , y } e. _V <-> { x , B } e. _V ) )
3		zfpair2 4188	. . . . 5 |- { x , y } e. _V
4	2, 3	vtoclg 2786	. . . 4 |- ( B e. W -> { x , B } e. _V )
5		preq1 3653	. . . . 5 |- ( x = A -> { x , B } = { A , B } )
6	5	eleq1d 2235	. . . 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 2797	. 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 1343   e. wcel 2136   _Vcvv 2726   {cpr 3577

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-14 2139  ax-ext 2147  ax-sep 4100  ax-pr 4187

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-v 2728  df-un 3120  df-sn 3582  df-pr 3583

This theorem is referenced by:  prelpwi  4192  opexg  4206  opi2  4211  opth  4215  opeqsn  4230  opeqpr  4231  uniop  4233  unex  4419  tpexg  4422  op1stb  4456  op1stbg  4457  onun2  4467  opthreg  4533  relop  4754  acexmidlemv  5840  pr2ne  7148  exmidonfinlem  7149  exmidaclem  7164  sup3exmid  8852  xrex  9792  2strbasg  12496  2stropg  12497  isomninnlem  13909  trilpolemlt1  13920  iswomninnlem  13928  iswomni0  13930  ismkvnnlem  13931