Theorem opexg 4314

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 3855	. 2 |- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
2		elex 2811	. . . . 5 |- ( A e. V -> A e. _V )
3		snexg 4268	. . . . 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 2811	. . . 4 |- ( B e. W -> B e. _V )
7		prexg 4295	. . . 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 4295	. . 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 2306	1 |- ( ( A e. V /\ B e. W ) -> <. A , B >. e. _V )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2200   _Vcvv 2799   {csn 3666   {cpr 3667   <.cop 3669

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675

This theorem is referenced by:  opex  4315  otexg  4316  opeliunxp  4774  opbrop  4798  relsnopg  4823  opswapg  5215  elxp4  5216  elxp5  5217  resfunexg  5864  fliftel  5923  fliftel1  5924  oprabid  6039  ovexg  6041  ovssunirng  6042  eloprabga  6097  op1st  6298  op2nd  6299  ot1stg  6304  ot2ndg  6305  ot3rdgg  6306  elxp6  6321  mpofvex  6357  algrflem  6381  algrflemg  6382  mpoxopoveq  6392  brtposg  6406  tfr0dm  6474  tfrlemisucaccv  6477  tfrlemibxssdm  6479  tfrlemibfn  6480  tfrlemi14d  6485  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfr1onlemres  6501  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllembfn  6509  tfrcllemres  6514  en2prd  6978  fnfi  7114  djulclb  7233  inl11  7243  1stinl  7252  2ndinl  7253  1stinr  7254  2ndinr  7255  mulpipq2  7569  enq0breq  7634  addvalex  8042  peano2nnnn  8051  axcnre  8079  frec2uzrdg  10643  frecuzrdg0  10647  frecuzrdgg  10650  frecuzrdg0t  10656  zfz1isolem1  11075  s1leng  11172  s111  11179  pfxclz  11227  eucalgval2  12591  crth  12762  phimullem  12763  ennnfonelemp1  12993  setsvala  13079  setsex  13080  setsfun  13083  setsfun0  13084  setsresg  13086  setscom  13088  strslfv  13093  strslfv3  13094  setsslid  13099  bassetsnn  13105  strle1g  13155  1strbas  13166  2strbasg  13169  2stropg  13170  2strbas1g  13172  2strop1g  13173  rngbaseg  13185  rngplusgg  13186  rngmulrg  13187  srngbased  13196  srngplusgd  13197  srngmulrd  13198  srnginvld  13199  lmodbased  13214  lmodplusgd  13215  lmodscad  13216  lmodvscad  13217  ipsbased  13226  ipsaddgd  13227  ipsmulrd  13228  ipsscad  13229  ipsvscad  13230  ipsipd  13231  topgrpbasd  13246  topgrpplusgd  13247  topgrptsetd  13248  prdsex  13318  prdsval  13322  imasex  13354  imasival  13355  imasbas  13356  imasplusg  13357  imasmulr  13358  imasaddfnlemg  13363  imasaddvallemg  13364  xpsfval  13397  xpsval  13401  intopsn  13416  mgm1  13419  sgrp1  13460  mnd1  13504  mnd1id  13505  grp1  13655  grp1inv  13656  ring1  14038  psrval  14646  fnpsr  14647  psrbasg  14654  psrplusgg  14658  txlm  14969  struct2slots2dom  15855  structvtxval  15856  structiedg0val  15857  structgrssvtx  15859  structgrssiedg  15860  gropd  15864  edgopval  15878  edgstruct  15880  isuhgropm  15897  uhgrunop  15903  upgrop  15920  upgr0eop  15938  upgr1eopdc  15939  upgrunop  15941  umgrunop  15943  isuspgropen  15978  isusgropen  15979  ausgrusgrben  15982  vtxdgop  16052