Theorem opexg 4370

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 3902	. 2 |- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
2		elex 2833	. . . . 5 |- ( A e. V -> A e. _V )
3		snexg 4323	. . . . 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 4351	. . . 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 4351	. . 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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209   _Vcvv 2821   {csn 3709   {cpr 3710   <.cop 3712

This proof depends on 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 4251  ax-pow 4313  ax-pr 4348

This proof 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 3715  df-pr 3716  df-op 3718

This theorem is used by:  opex  4371  otexg  4372  opeliunxp  4832  opbrop  4856  relsnopg  4881  opswapg  5277  elxp4  5278  elxp5  5279  resfunexg  5939  fliftel  6002  fliftel1  6003  oprabid  6120  ovexg  6122  ovssunirng  6123  eloprabga  6178  op1st  6384  op2nd  6385  ot1stg  6390  ot2ndg  6391  ot3rdgg  6392  elxp6  6407  mpofvex  6445  algrflem  6469  algrflemg  6470  mpoxopoveq  6516  brtposg  6530  tfr0dm  6598  tfrlemisucaccv  6601  tfrlemibxssdm  6603  tfrlemibfn  6604  tfrlemi14d  6609  tfr1onlemsucaccv  6617  tfr1onlembxssdm  6619  tfr1onlembfn  6620  tfr1onlemres  6625  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllembfn  6633  tfrcllemres  6638  mapsnend  7105  en2prd  7112  fnfi  7256  snopfsupp  7306  djulclb  7401  inl11  7411  1stinl  7420  2ndinl  7421  1stinr  7422  2ndinr  7423  mulpipq2  7744  enq0breq  7809  addvalex  8217  peano2nnnn  8226  axcnre  8254  frec2uzrdg  10866  frecuzrdg0  10870  frecuzrdgg  10873  frecuzrdg0t  10879  zfz1isolem1  11313  s1leng  11413  s111  11420  pfxclz  11472  eucalgval2  12855  crth  13030  phimullem  13031  ennnfonelemp1  13354  setsvala  13440  setsex  13441  setsfun  13444  setsfun0  13445  setsresg  13447  setscom  13449  strslfv  13454  strslfv3  13455  setsslid  13460  bassetsnn  13466  strle1g  13518  1strbas  13529  2strbasg  13532  2stropg  13533  2strbas1g  13535  2strop1g  13536  rngbaseg  13548  rngplusgg  13549  rngmulrg  13550  srngbased  13559  srngplusgd  13560  srngmulrd  13561  srnginvld  13562  lmodbased  13577  lmodplusgd  13578  lmodscad  13579  lmodvscad  13580  ipsbased  13589  ipsaddgd  13590  ipsmulrd  13591  ipsscad  13592  ipsvscad  13593  ipsipd  13594  topgrpbasd  13609  topgrpplusgd  13610  topgrptsetd  13611  imasex  13684  imasival  13685  imasbas  13686  imasplusg  13687  imasmulr  13688  imasaddfnlemg  13693  imasaddvallemg  13694  xpsfval  13727  intopsn  13745  mgm1  13748  sgrp1  13784  mnd1  13820  mnd1id  13821  grp1  13969  grp1inv  13970  prdsex  14278  prdsval  14279  xpsval  14307  ring1  14470  psrval  15160  fnpsr  15161  psrbasg  15187  psrplusgg  15191  txlm  15522  struct2slots2dom  16501  structvtxval  16502  structiedg0val  16503  structgrssvtx  16505  structgrssiedg  16506  gropd  16510  edgopval  16525  edgstruct  16527  isuhgropm  16544  uhgrunop  16550  upgrop  16567  upgr0eop  16585  upgr1eopdc  16586  upgr1een  16587  umgr1een  16588  upgrunop  16590  umgrunop  16592  isuspgropen  16627  isusgropen  16628  ausgrusgrben  16631  usgr0eop  16705  uspgr1eopdc  16706  usgr1eop  16708  uhgrspanop  16745  vtxdgop  16755  p1evtxdeqfilem  16774  p1evtxdeqfi  16775  p1evtxdp1fi  16776  eupthvdres  16938  eupth2lem3fi  16939  konigsbergumgr  16950