Theorem opexg 4320

Description: An ordered pair of sets is a set. (Contributed by Jim Kingdon, 11-Jan-2019.)

Assertion

Ref	Expression
opexg	|- ( ( A e. V /\ B e. W ) -> <. A , B >. e. _V )

Proof of Theorem opexg

Step	Hyp	Ref	Expression
1		dfopg 3860	. 2 |- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
2		elex 2814	. . . . 5 |- ( A e. V -> A e. _V )
3		snexg 4274	. . . . 5 |- ( A e. _V -> { A } e. _V )
4	2, 3	syl 14	. . . 4 |- ( A e. V -> { A } e. _V )
5	4	adantr 276	. . 3 |- ( ( A e. V /\ B e. W ) -> { A } e. _V )
6		elex 2814	. . . 4 |- ( B e. W -> B e. _V )
7		prexg 4301	. . . 4 |- ( ( A e. _V /\ B e. _V ) -> { A , B } e. _V )
8	2, 6, 7	syl2an 289	. . 3 |- ( ( A e. V /\ B e. W ) -> { A , B } e. _V )
9		prexg 4301	. . 3 |- ( ( { A } e. _V /\ { A , B } e. _V ) -> { { A } , { A , B } } e. _V )
10	5, 8, 9	syl2anc 411	. 2 |- ( ( A e. V /\ B e. W ) -> { { A } , { A , B } } e. _V )
11	1, 10	eqeltrd 2308	1 |- ( ( A e. V /\ B e. W ) -> <. A , B >. e. _V )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2202   _Vcvv 2802   {csn 3669   {cpr 3670   <.cop 3672

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678

This theorem is referenced by:  opex  4321  otexg  4322  opeliunxp  4781  opbrop  4805  relsnopg  4830  opswapg  5223  elxp4  5224  elxp5  5225  resfunexg  5876  fliftel  5937  fliftel1  5938  oprabid  6053  ovexg  6055  ovssunirng  6056  eloprabga  6111  op1st  6312  op2nd  6313  ot1stg  6318  ot2ndg  6319  ot3rdgg  6320  elxp6  6335  mpofvex  6373  algrflem  6397  algrflemg  6398  mpoxopoveq  6409  brtposg  6423  tfr0dm  6491  tfrlemisucaccv  6494  tfrlemibxssdm  6496  tfrlemibfn  6497  tfrlemi14d  6502  tfr1onlemsucaccv  6510  tfr1onlembxssdm  6512  tfr1onlembfn  6513  tfr1onlemres  6518  tfrcllemsucaccv  6523  tfrcllembxssdm  6525  tfrcllembfn  6526  tfrcllemres  6531  en2prd  6995  fnfi  7138  djulclb  7257  inl11  7267  1stinl  7276  2ndinl  7277  1stinr  7278  2ndinr  7279  mulpipq2  7594  enq0breq  7659  addvalex  8067  peano2nnnn  8076  axcnre  8104  frec2uzrdg  10675  frecuzrdg0  10679  frecuzrdgg  10682  frecuzrdg0t  10688  zfz1isolem1  11108  s1leng  11208  s111  11215  pfxclz  11267  eucalgval2  12646  crth  12817  phimullem  12818  ennnfonelemp1  13048  setsvala  13134  setsex  13135  setsfun  13138  setsfun0  13139  setsresg  13141  setscom  13143  strslfv  13148  strslfv3  13149  setsslid  13154  bassetsnn  13160  strle1g  13210  1strbas  13221  2strbasg  13224  2stropg  13225  2strbas1g  13227  2strop1g  13228  rngbaseg  13240  rngplusgg  13241  rngmulrg  13242  srngbased  13251  srngplusgd  13252  srngmulrd  13253  srnginvld  13254  lmodbased  13269  lmodplusgd  13270  lmodscad  13271  lmodvscad  13272  ipsbased  13281  ipsaddgd  13282  ipsmulrd  13283  ipsscad  13284  ipsvscad  13285  ipsipd  13286  topgrpbasd  13301  topgrpplusgd  13302  topgrptsetd  13303  prdsex  13373  prdsval  13377  imasex  13409  imasival  13410  imasbas  13411  imasplusg  13412  imasmulr  13413  imasaddfnlemg  13418  imasaddvallemg  13419  xpsfval  13452  xpsval  13456  intopsn  13471  mgm1  13474  sgrp1  13515  mnd1  13559  mnd1id  13560  grp1  13710  grp1inv  13711  ring1  14094  psrval  14702  fnpsr  14703  psrbasg  14715  psrplusgg  14719  txlm  15030  struct2slots2dom  15916  structvtxval  15917  structiedg0val  15918  structgrssvtx  15920  structgrssiedg  15921  gropd  15925  edgopval  15940  edgstruct  15942  isuhgropm  15959  uhgrunop  15965  upgrop  15982  upgr0eop  16000  upgr1eopdc  16001  upgr1een  16002  umgr1een  16003  upgrunop  16005  umgrunop  16007  isuspgropen  16042  isusgropen  16043  ausgrusgrben  16046  usgr0eop  16120  uspgr1eopdc  16121  usgr1eop  16123  uhgrspanop  16160  vtxdgop  16170  p1evtxdeqfilem  16189  p1evtxdeqfi  16190  p1evtxdp1fi  16191  eupthvdres  16353  eupth2lem3fi  16354  konigsbergumgr  16365