Theorem opexg 4318

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 3858	. 2 |- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
2		elex 2812	. . . . 5 |- ( A e. V -> A e. _V )
3		snexg 4272	. . . . 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 2812	. . . 4 |- ( B e. W -> B e. _V )
7		prexg 4299	. . . 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 4299	. . 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 2800   {csn 3667   {cpr 3668   <.cop 3670

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 4205  ax-pow 4262  ax-pr 4297

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 2802  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676

This theorem is referenced by:  opex  4319  otexg  4320  opeliunxp  4779  opbrop  4803  relsnopg  4828  opswapg  5221  elxp4  5222  elxp5  5223  resfunexg  5870  fliftel  5929  fliftel1  5930  oprabid  6045  ovexg  6047  ovssunirng  6048  eloprabga  6103  op1st  6304  op2nd  6305  ot1stg  6310  ot2ndg  6311  ot3rdgg  6312  elxp6  6327  mpofvex  6365  algrflem  6389  algrflemg  6390  mpoxopoveq  6401  brtposg  6415  tfr0dm  6483  tfrlemisucaccv  6486  tfrlemibxssdm  6488  tfrlemibfn  6489  tfrlemi14d  6494  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfr1onlemres  6510  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllembfn  6518  tfrcllemres  6523  en2prd  6987  fnfi  7126  djulclb  7245  inl11  7255  1stinl  7264  2ndinl  7265  1stinr  7266  2ndinr  7267  mulpipq2  7581  enq0breq  7646  addvalex  8054  peano2nnnn  8063  axcnre  8091  frec2uzrdg  10661  frecuzrdg0  10665  frecuzrdgg  10668  frecuzrdg0t  10674  zfz1isolem1  11094  s1leng  11191  s111  11198  pfxclz  11250  eucalgval2  12615  crth  12786  phimullem  12787  ennnfonelemp1  13017  setsvala  13103  setsex  13104  setsfun  13107  setsfun0  13108  setsresg  13110  setscom  13112  strslfv  13117  strslfv3  13118  setsslid  13123  bassetsnn  13129  strle1g  13179  1strbas  13190  2strbasg  13193  2stropg  13194  2strbas1g  13196  2strop1g  13197  rngbaseg  13209  rngplusgg  13210  rngmulrg  13211  srngbased  13220  srngplusgd  13221  srngmulrd  13222  srnginvld  13223  lmodbased  13238  lmodplusgd  13239  lmodscad  13240  lmodvscad  13241  ipsbased  13250  ipsaddgd  13251  ipsmulrd  13252  ipsscad  13253  ipsvscad  13254  ipsipd  13255  topgrpbasd  13270  topgrpplusgd  13271  topgrptsetd  13272  prdsex  13342  prdsval  13346  imasex  13378  imasival  13379  imasbas  13380  imasplusg  13381  imasmulr  13382  imasaddfnlemg  13387  imasaddvallemg  13388  xpsfval  13421  xpsval  13425  intopsn  13440  mgm1  13443  sgrp1  13484  mnd1  13528  mnd1id  13529  grp1  13679  grp1inv  13680  ring1  14062  psrval  14670  fnpsr  14671  psrbasg  14678  psrplusgg  14682  txlm  14993  struct2slots2dom  15879  structvtxval  15880  structiedg0val  15881  structgrssvtx  15883  structgrssiedg  15884  gropd  15888  edgopval  15903  edgstruct  15905  isuhgropm  15922  uhgrunop  15928  upgrop  15945  upgr0eop  15963  upgr1eopdc  15964  upgrunop  15966  umgrunop  15968  isuspgropen  16003  isusgropen  16004  ausgrusgrben  16007  usgr0eop  16081  uspgr1eopdc  16082  usgr1eop  16084  vtxdgop  16098