Theorem opexg 4346

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 3883	. 2 |- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
2		elex 2827	. . . . 5 |- ( A e. V -> A e. _V )
3		snexg 4299	. . . . 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 2827	. . . 4 |- ( B e. W -> B e. _V )
7		prexg 4327	. . . 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 4327	. . 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 2311	1 |- ( ( A e. V /\ B e. W ) -> <. A , B >. e. _V )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2205   _Vcvv 2815   {csn 3691   {cpr 3692   <.cop 3694

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2208  ax-ext 2216  ax-sep 4230  ax-pow 4289  ax-pr 4324

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3217  df-in 3219  df-ss 3226  df-pw 3673  df-sn 3697  df-pr 3698  df-op 3700

This theorem is referenced by:  opex  4347  otexg  4348  opeliunxp  4807  opbrop  4831  relsnopg  4856  opswapg  5251  elxp4  5252  elxp5  5253  resfunexg  5907  fliftel  5968  fliftel1  5969  oprabid  6084  ovexg  6086  ovssunirng  6087  eloprabga  6142  op1st  6342  op2nd  6343  ot1stg  6348  ot2ndg  6349  ot3rdgg  6350  elxp6  6365  mpofvex  6403  algrflem  6427  algrflemg  6428  mpoxopoveq  6473  brtposg  6487  tfr0dm  6555  tfrlemisucaccv  6558  tfrlemibxssdm  6560  tfrlemibfn  6561  tfrlemi14d  6566  tfr1onlemsucaccv  6574  tfr1onlembxssdm  6576  tfr1onlembfn  6577  tfr1onlemres  6582  tfrcllemsucaccv  6587  tfrcllembxssdm  6589  tfrcllembfn  6590  tfrcllemres  6595  mapsnend  7054  en2prd  7061  fnfi  7205  snopfsuppdc  7254  djulclb  7348  inl11  7358  1stinl  7367  2ndinl  7368  1stinr  7369  2ndinr  7370  mulpipq2  7688  enq0breq  7753  addvalex  8161  peano2nnnn  8170  axcnre  8198  frec2uzrdg  10775  frecuzrdg0  10779  frecuzrdgg  10782  frecuzrdg0t  10788  zfz1isolem1  11216  s1leng  11316  s111  11323  pfxclz  11375  eucalgval2  12754  crth  12925  phimullem  12926  ennnfonelemp1  13174  setsvala  13260  setsex  13261  setsfun  13264  setsfun0  13265  setsresg  13267  setscom  13269  strslfv  13274  strslfv3  13275  setsslid  13280  bassetsnn  13286  strle1g  13336  1strbas  13347  2strbasg  13350  2stropg  13351  2strbas1g  13353  2strop1g  13354  rngbaseg  13366  rngplusgg  13367  rngmulrg  13368  srngbased  13377  srngplusgd  13378  srngmulrd  13379  srnginvld  13380  lmodbased  13395  lmodplusgd  13396  lmodscad  13397  lmodvscad  13398  ipsbased  13407  ipsaddgd  13408  ipsmulrd  13409  ipsscad  13410  ipsvscad  13411  ipsipd  13412  topgrpbasd  13427  topgrpplusgd  13428  topgrptsetd  13429  prdsex  13499  prdsval  13503  imasex  13535  imasival  13536  imasbas  13537  imasplusg  13538  imasmulr  13539  imasaddfnlemg  13544  imasaddvallemg  13545  xpsfval  13578  xpsval  13582  intopsn  13597  mgm1  13600  sgrp1  13641  mnd1  13685  mnd1id  13686  grp1  13836  grp1inv  13837  ring1  14220  psrval  14831  fnpsr  14832  psrbasg  14846  psrplusgg  14850  txlm  15161  struct2slots2dom  16050  structvtxval  16051  structiedg0val  16052  structgrssvtx  16054  structgrssiedg  16055  gropd  16059  edgopval  16074  edgstruct  16076  isuhgropm  16093  uhgrunop  16099  upgrop  16116  upgr0eop  16134  upgr1eopdc  16135  upgr1een  16136  umgr1een  16137  upgrunop  16139  umgrunop  16141  isuspgropen  16176  isusgropen  16177  ausgrusgrben  16180  usgr0eop  16254  uspgr1eopdc  16255  usgr1eop  16257  uhgrspanop  16294  vtxdgop  16304  p1evtxdeqfilem  16323  p1evtxdeqfi  16324  p1evtxdp1fi  16325  eupthvdres  16487  eupth2lem3fi  16488  konigsbergumgr  16499