Theorem opexg 4349

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 3886	. 2 |- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
2		elex 2827	. . . . 5 |- ( A e. V -> A e. _V )
3		snexg 4302	. . . . 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 2827	. . . 4 |- ( B e. W -> B e. _V )
7		prexg 4330	. . . 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 4330	. . 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 2311	1 |- ( ( A e. V /\ B e. W ) -> <. A , B >. e. _V )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2205   _Vcvv 2815   {csn 3694   {cpr 3695   <.cop 3697

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-pr 4327

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703

This theorem is referenced by:  opex  4350  otexg  4351  opeliunxp  4810  opbrop  4834  relsnopg  4859  opswapg  5254  elxp4  5255  elxp5  5256  resfunexg  5910  fliftel  5972  fliftel1  5973  oprabid  6090  ovexg  6092  ovssunirng  6093  eloprabga  6148  op1st  6353  op2nd  6354  ot1stg  6359  ot2ndg  6360  ot3rdgg  6361  elxp6  6376  mpofvex  6414  algrflem  6438  algrflemg  6439  mpoxopoveq  6484  brtposg  6498  tfr0dm  6566  tfrlemisucaccv  6569  tfrlemibxssdm  6571  tfrlemibfn  6572  tfrlemi14d  6577  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfr1onlemres  6593  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllembfn  6601  tfrcllemres  6606  mapsnend  7065  en2prd  7072  fnfi  7216  snopfsuppdc  7265  djulclb  7359  inl11  7369  1stinl  7378  2ndinl  7379  1stinr  7380  2ndinr  7381  mulpipq2  7702  enq0breq  7767  addvalex  8175  peano2nnnn  8184  axcnre  8212  frec2uzrdg  10795  frecuzrdg0  10799  frecuzrdgg  10802  frecuzrdg0t  10808  zfz1isolem1  11237  s1leng  11337  s111  11344  pfxclz  11396  eucalgval2  12775  crth  12946  phimullem  12947  ennnfonelemp1  13241  setsvala  13327  setsex  13328  setsfun  13331  setsfun0  13332  setsresg  13334  setscom  13336  strslfv  13341  strslfv3  13342  setsslid  13347  bassetsnn  13353  strle1g  13403  1strbas  13414  2strbasg  13417  2stropg  13418  2strbas1g  13420  2strop1g  13421  rngbaseg  13433  rngplusgg  13434  rngmulrg  13435  srngbased  13444  srngplusgd  13445  srngmulrd  13446  srnginvld  13447  lmodbased  13462  lmodplusgd  13463  lmodscad  13464  lmodvscad  13465  ipsbased  13474  ipsaddgd  13475  ipsmulrd  13476  ipsscad  13477  ipsvscad  13478  ipsipd  13479  topgrpbasd  13494  topgrpplusgd  13495  topgrptsetd  13496  imasex  13569  imasival  13570  imasbas  13571  imasplusg  13572  imasmulr  13573  imasaddfnlemg  13578  imasaddvallemg  13579  xpsfval  13612  intopsn  13630  mgm1  13633  sgrp1  13674  mnd1  13710  mnd1id  13711  grp1  13861  grp1inv  13862  prdsex  14114  prdsval  14115  xpsval  14143  ring1  14302  psrval  14940  fnpsr  14941  psrbasg  14955  psrplusgg  14959  txlm  15270  struct2slots2dom  16159  structvtxval  16160  structiedg0val  16161  structgrssvtx  16163  structgrssiedg  16164  gropd  16168  edgopval  16183  edgstruct  16185  isuhgropm  16202  uhgrunop  16208  upgrop  16225  upgr0eop  16243  upgr1eopdc  16244  upgr1een  16245  umgr1een  16246  upgrunop  16248  umgrunop  16250  isuspgropen  16285  isusgropen  16286  ausgrusgrben  16289  usgr0eop  16363  uspgr1eopdc  16364  usgr1eop  16366  uhgrspanop  16403  vtxdgop  16413  p1evtxdeqfilem  16432  p1evtxdeqfi  16433  p1evtxdp1fi  16434  eupthvdres  16596  eupth2lem3fi  16597  konigsbergumgr  16608