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  6515  brtposg  6529  tfr0dm  6597  tfrlemisucaccv  6600  tfrlemibxssdm  6602  tfrlemibfn  6603  tfrlemi14d  6608  tfr1onlemsucaccv  6616  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfr1onlemres  6624  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllembfn  6632  tfrcllemres  6637  mapsnend  7103  en2prd  7110  fnfi  7254  snopfsuppdc  7304  djulclb  7401  inl11  7411  1stinl  7420  2ndinl  7421  1stinr  7422  2ndinr  7423  mulpipq2  7744  enq0breq  7809  addvalex  8217  peano2nnnn  8226  axcnre  8254  frec2uzrdg  10867  frecuzrdg0  10871  frecuzrdgg  10874  frecuzrdg0t  10880  zfz1isolem1  11314  s1leng  11414  s111  11421  pfxclz  11473  eucalgval2  12856  crth  13031  phimullem  13032  ennnfonelemp1  13355  setsvala  13441  setsex  13442  setsfun  13445  setsfun0  13446  setsresg  13448  setscom  13450  strslfv  13455  strslfv3  13456  setsslid  13461  bassetsnn  13467  strle1g  13519  1strbas  13530  2strbasg  13533  2stropg  13534  2strbas1g  13536  2strop1g  13537  rngbaseg  13549  rngplusgg  13550  rngmulrg  13551  srngbased  13560  srngplusgd  13561  srngmulrd  13562  srnginvld  13563  lmodbased  13578  lmodplusgd  13579  lmodscad  13580  lmodvscad  13581  ipsbased  13590  ipsaddgd  13591  ipsmulrd  13592  ipsscad  13593  ipsvscad  13594  ipsipd  13595  topgrpbasd  13610  topgrpplusgd  13611  topgrptsetd  13612  imasex  13685  imasival  13686  imasbas  13687  imasplusg  13688  imasmulr  13689  imasaddfnlemg  13694  imasaddvallemg  13695  xpsfval  13728  intopsn  13746  mgm1  13749  sgrp1  13785  mnd1  13821  mnd1id  13822  grp1  13970  grp1inv  13971  prdsex  14279  prdsval  14280  xpsval  14308  ring1  14471  psrval  15159  fnpsr  15160  psrbasg  15178  psrplusgg  15182  txlm  15505  struct2slots2dom  16484  structvtxval  16485  structiedg0val  16486  structgrssvtx  16488  structgrssiedg  16489  gropd  16493  edgopval  16508  edgstruct  16510  isuhgropm  16527  uhgrunop  16533  upgrop  16550  upgr0eop  16568  upgr1eopdc  16569  upgr1een  16570  umgr1een  16571  upgrunop  16573  umgrunop  16575  isuspgropen  16610  isusgropen  16611  ausgrusgrben  16614  usgr0eop  16688  uspgr1eopdc  16689  usgr1eop  16691  uhgrspanop  16728  vtxdgop  16738  p1evtxdeqfilem  16757  p1evtxdeqfi  16758  p1evtxdp1fi  16759  eupthvdres  16921  eupth2lem3fi  16922  konigsbergumgr  16933