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  5874  fliftel  5933  fliftel1  5934  oprabid  6049  ovexg  6051  ovssunirng  6052  eloprabga  6107  op1st  6308  op2nd  6309  ot1stg  6314  ot2ndg  6315  ot3rdgg  6316  elxp6  6331  mpofvex  6369  algrflem  6393  algrflemg  6394  mpoxopoveq  6405  brtposg  6419  tfr0dm  6487  tfrlemisucaccv  6490  tfrlemibxssdm  6492  tfrlemibfn  6493  tfrlemi14d  6498  tfr1onlemsucaccv  6506  tfr1onlembxssdm  6508  tfr1onlembfn  6509  tfr1onlemres  6514  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllembfn  6522  tfrcllemres  6527  en2prd  6991  fnfi  7134  djulclb  7253  inl11  7263  1stinl  7272  2ndinl  7273  1stinr  7274  2ndinr  7275  mulpipq2  7590  enq0breq  7655  addvalex  8063  peano2nnnn  8072  axcnre  8100  frec2uzrdg  10670  frecuzrdg0  10674  frecuzrdgg  10677  frecuzrdg0t  10683  zfz1isolem1  11103  s1leng  11200  s111  11207  pfxclz  11259  eucalgval2  12624  crth  12795  phimullem  12796  ennnfonelemp1  13026  setsvala  13112  setsex  13113  setsfun  13116  setsfun0  13117  setsresg  13119  setscom  13121  strslfv  13126  strslfv3  13127  setsslid  13132  bassetsnn  13138  strle1g  13188  1strbas  13199  2strbasg  13202  2stropg  13203  2strbas1g  13205  2strop1g  13206  rngbaseg  13218  rngplusgg  13219  rngmulrg  13220  srngbased  13229  srngplusgd  13230  srngmulrd  13231  srnginvld  13232  lmodbased  13247  lmodplusgd  13248  lmodscad  13249  lmodvscad  13250  ipsbased  13259  ipsaddgd  13260  ipsmulrd  13261  ipsscad  13262  ipsvscad  13263  ipsipd  13264  topgrpbasd  13279  topgrpplusgd  13280  topgrptsetd  13281  prdsex  13351  prdsval  13355  imasex  13387  imasival  13388  imasbas  13389  imasplusg  13390  imasmulr  13391  imasaddfnlemg  13396  imasaddvallemg  13397  xpsfval  13430  xpsval  13434  intopsn  13449  mgm1  13452  sgrp1  13493  mnd1  13537  mnd1id  13538  grp1  13688  grp1inv  13689  ring1  14071  psrval  14679  fnpsr  14680  psrbasg  14687  psrplusgg  14691  txlm  15002  struct2slots2dom  15888  structvtxval  15889  structiedg0val  15890  structgrssvtx  15892  structgrssiedg  15893  gropd  15897  edgopval  15912  edgstruct  15914  isuhgropm  15931  uhgrunop  15937  upgrop  15954  upgr0eop  15972  upgr1eopdc  15973  upgr1een  15974  umgr1een  15975  upgrunop  15977  umgrunop  15979  isuspgropen  16014  isusgropen  16015  ausgrusgrben  16018  usgr0eop  16092  uspgr1eopdc  16093  usgr1eop  16095  uhgrspanop  16132  vtxdgop  16142  p1evtxdeqfilem  16161  p1evtxdeqfi  16162  p1evtxdp1fi  16163