Theorem opexg 4368

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 4321	. . . . 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 4349	. . . 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 4349	. . 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 4249  ax-pow 4311  ax-pr 4346

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  4369  otexg  4370  opeliunxp  4830  opbrop  4854  relsnopg  4879  opswapg  5274  elxp4  5275  elxp5  5276  resfunexg  5936  fliftel  5999  fliftel1  6000  oprabid  6117  ovexg  6119  ovssunirng  6120  eloprabga  6175  op1st  6380  op2nd  6381  ot1stg  6386  ot2ndg  6387  ot3rdgg  6388  elxp6  6403  mpofvex  6441  algrflem  6465  algrflemg  6466  mpoxopoveq  6511  brtposg  6525  tfr0dm  6593  tfrlemisucaccv  6596  tfrlemibxssdm  6598  tfrlemibfn  6599  tfrlemi14d  6604  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemres  6620  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemres  6633  mapsnend  7099  en2prd  7106  fnfi  7250  snopfsuppdc  7299  djulclb  7396  inl11  7406  1stinl  7415  2ndinl  7416  1stinr  7417  2ndinr  7418  mulpipq2  7739  enq0breq  7804  addvalex  8212  peano2nnnn  8221  axcnre  8249  frec2uzrdg  10861  frecuzrdg0  10865  frecuzrdgg  10868  frecuzrdg0t  10874  zfz1isolem1  11308  s1leng  11408  s111  11415  pfxclz  11467  eucalgval2  12850  crth  13025  phimullem  13026  ennnfonelemp1  13349  setsvala  13435  setsex  13436  setsfun  13439  setsfun0  13440  setsresg  13442  setscom  13444  strslfv  13449  strslfv3  13450  setsslid  13455  bassetsnn  13461  strle1g  13513  1strbas  13524  2strbasg  13527  2stropg  13528  2strbas1g  13530  2strop1g  13531  rngbaseg  13543  rngplusgg  13544  rngmulrg  13545  srngbased  13554  srngplusgd  13555  srngmulrd  13556  srnginvld  13557  lmodbased  13572  lmodplusgd  13573  lmodscad  13574  lmodvscad  13575  ipsbased  13584  ipsaddgd  13585  ipsmulrd  13586  ipsscad  13587  ipsvscad  13588  ipsipd  13589  topgrpbasd  13604  topgrpplusgd  13605  topgrptsetd  13606  imasex  13679  imasival  13680  imasbas  13681  imasplusg  13682  imasmulr  13683  imasaddfnlemg  13688  imasaddvallemg  13689  xpsfval  13722  intopsn  13740  mgm1  13743  sgrp1  13779  mnd1  13815  mnd1id  13816  grp1  13964  grp1inv  13965  prdsex  14256  prdsval  14257  xpsval  14285  ring1  14448  psrval  15134  fnpsr  15135  psrbasg  15150  psrplusgg  15154  txlm  15471  struct2slots2dom  16445  structvtxval  16446  structiedg0val  16447  structgrssvtx  16449  structgrssiedg  16450  gropd  16454  edgopval  16469  edgstruct  16471  isuhgropm  16488  uhgrunop  16494  upgrop  16511  upgr0eop  16529  upgr1eopdc  16530  upgr1een  16531  umgr1een  16532  upgrunop  16534  umgrunop  16536  isuspgropen  16571  isusgropen  16572  ausgrusgrben  16575  usgr0eop  16649  uspgr1eopdc  16650  usgr1eop  16652  uhgrspanop  16689  vtxdgop  16699  p1evtxdeqfilem  16718  p1evtxdeqfi  16719  p1evtxdp1fi  16720  eupthvdres  16882  eupth2lem3fi  16883  konigsbergumgr  16894