Theorem opexg 4366

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 3900	. 2 |- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
2		elex 2833	. . . . 5 |- ( A e. V -> A e. _V )
3		snexg 4319	. . . . 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 2833	. . . 4 |- ( B e. W -> B e. _V )
7		prexg 4347	. . . 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 4347	. . 3 |- ( ( { A } e. _V /\ { A , B } e. _V ) -> { { A } , { A , B } } e. _V )
10	5, 8, 9	syl2anc 415	. 2 |- ( ( A e. V /\ B e. W ) -> { { A } , { A , B } } e. _V )
11	1, 10	eqeltrd 2315	1 |- ( ( A e. V /\ B e. W ) -> <. A , B >. e. _V )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2209   _Vcvv 2821   {csn 3708   {cpr 3709   <.cop 3711

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4247  ax-pow 4309  ax-pr 4344

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3714  df-pr 3715  df-op 3717

This theorem is referenced by:  opex  4367  otexg  4368  opeliunxp  4828  opbrop  4852  relsnopg  4877  opswapg  5272  elxp4  5273  elxp5  5274  resfunexg  5930  fliftel  5992  fliftel1  5993  oprabid  6110  ovexg  6112  ovssunirng  6113  eloprabga  6168  op1st  6373  op2nd  6374  ot1stg  6379  ot2ndg  6380  ot3rdgg  6381  elxp6  6396  mpofvex  6434  algrflem  6458  algrflemg  6459  mpoxopoveq  6504  brtposg  6518  tfr0dm  6586  tfrlemisucaccv  6589  tfrlemibxssdm  6591  tfrlemibfn  6592  tfrlemi14d  6597  tfr1onlemsucaccv  6605  tfr1onlembxssdm  6607  tfr1onlembfn  6608  tfr1onlemres  6613  tfrcllemsucaccv  6618  tfrcllembxssdm  6620  tfrcllembfn  6621  tfrcllemres  6626  mapsnend  7092  en2prd  7099  fnfi  7243  snopfsuppdc  7292  djulclb  7388  inl11  7398  1stinl  7407  2ndinl  7408  1stinr  7409  2ndinr  7410  mulpipq2  7731  enq0breq  7796  addvalex  8204  peano2nnnn  8213  axcnre  8241  frec2uzrdg  10827  frecuzrdg0  10831  frecuzrdgg  10834  frecuzrdg0t  10840  zfz1isolem1  11273  s1leng  11373  s111  11380  pfxclz  11432  eucalgval2  12812  crth  12983  phimullem  12984  ennnfonelemp1  13278  setsvala  13364  setsex  13365  setsfun  13368  setsfun0  13369  setsresg  13371  setscom  13373  strslfv  13378  strslfv3  13379  setsslid  13384  bassetsnn  13390  strle1g  13440  1strbas  13451  2strbasg  13454  2stropg  13455  2strbas1g  13457  2strop1g  13458  rngbaseg  13470  rngplusgg  13471  rngmulrg  13472  srngbased  13481  srngplusgd  13482  srngmulrd  13483  srnginvld  13484  lmodbased  13499  lmodplusgd  13500  lmodscad  13501  lmodvscad  13502  ipsbased  13511  ipsaddgd  13512  ipsmulrd  13513  ipsscad  13514  ipsvscad  13515  ipsipd  13516  topgrpbasd  13531  topgrpplusgd  13532  topgrptsetd  13533  imasex  13606  imasival  13607  imasbas  13608  imasplusg  13609  imasmulr  13610  imasaddfnlemg  13615  imasaddvallemg  13616  xpsfval  13649  intopsn  13667  mgm1  13670  sgrp1  13706  mnd1  13742  mnd1id  13743  grp1  13891  grp1inv  13892  prdsex  14152  prdsval  14153  xpsval  14181  ring1  14340  psrval  14976  fnpsr  14977  psrbasg  14991  psrplusgg  14995  txlm  15306  struct2slots2dom  16196  structvtxval  16197  structiedg0val  16198  structgrssvtx  16200  structgrssiedg  16201  gropd  16205  edgopval  16220  edgstruct  16222  isuhgropm  16239  uhgrunop  16245  upgrop  16262  upgr0eop  16280  upgr1eopdc  16281  upgr1een  16282  umgr1een  16283  upgrunop  16285  umgrunop  16287  isuspgropen  16322  isusgropen  16323  ausgrusgrben  16326  usgr0eop  16400  uspgr1eopdc  16401  usgr1eop  16403  uhgrspanop  16440  vtxdgop  16450  p1evtxdeqfilem  16469  p1evtxdeqfi  16470  p1evtxdp1fi  16471  eupthvdres  16633  eupth2lem3fi  16634  konigsbergumgr  16645