Theorem opexg 4290

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 3831	. 2 |- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
2		elex 2788	. . . . 5 |- ( A e. V -> A e. _V )
3		snexg 4244	. . . . 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 2788	. . . 4 |- ( B e. W -> B e. _V )
7		prexg 4271	. . . 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 4271	. . 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 2284	1 |- ( ( A e. V /\ B e. W ) -> <. A , B >. e. _V )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2178   _Vcvv 2776   {csn 3643   {cpr 3644   <.cop 3646

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pow 4234  ax-pr 4269

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-un 3178  df-in 3180  df-ss 3187  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652

This theorem is referenced by:  opex  4291  otexg  4292  opeliunxp  4748  opbrop  4772  relsnopg  4797  opswapg  5188  elxp4  5189  elxp5  5190  resfunexg  5828  fliftel  5885  fliftel1  5886  oprabid  5999  ovexg  6001  ovssunirng  6002  eloprabga  6055  op1st  6255  op2nd  6256  ot1stg  6261  ot2ndg  6262  ot3rdgg  6263  elxp6  6278  mpofvex  6314  algrflem  6338  algrflemg  6339  mpoxopoveq  6349  brtposg  6363  tfr0dm  6431  tfrlemisucaccv  6434  tfrlemibxssdm  6436  tfrlemibfn  6437  tfrlemi14d  6442  tfr1onlemsucaccv  6450  tfr1onlembxssdm  6452  tfr1onlembfn  6453  tfr1onlemres  6458  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  tfrcllembfn  6466  tfrcllemres  6471  en2prd  6933  fnfi  7064  djulclb  7183  inl11  7193  1stinl  7202  2ndinl  7203  1stinr  7204  2ndinr  7205  mulpipq2  7519  enq0breq  7584  addvalex  7992  peano2nnnn  8001  axcnre  8029  frec2uzrdg  10591  frecuzrdg0  10595  frecuzrdgg  10598  frecuzrdg0t  10604  zfz1isolem1  11022  s1leng  11116  s111  11123  pfxclz  11170  eucalgval2  12490  crth  12661  phimullem  12662  ennnfonelemp1  12892  setsvala  12978  setsex  12979  setsfun  12982  setsfun0  12983  setsresg  12985  setscom  12987  strslfv  12992  strslfv3  12993  setsslid  12998  strle1g  13053  1strbas  13064  2strbasg  13067  2stropg  13068  2strbas1g  13070  2strop1g  13071  rngbaseg  13083  rngplusgg  13084  rngmulrg  13085  srngbased  13094  srngplusgd  13095  srngmulrd  13096  srnginvld  13097  lmodbased  13112  lmodplusgd  13113  lmodscad  13114  lmodvscad  13115  ipsbased  13124  ipsaddgd  13125  ipsmulrd  13126  ipsscad  13127  ipsvscad  13128  ipsipd  13129  topgrpbasd  13144  topgrpplusgd  13145  topgrptsetd  13146  prdsex  13216  prdsval  13220  imasex  13252  imasival  13253  imasbas  13254  imasplusg  13255  imasmulr  13256  imasaddfnlemg  13261  imasaddvallemg  13262  xpsfval  13295  xpsval  13299  intopsn  13314  mgm1  13317  sgrp1  13358  mnd1  13402  mnd1id  13403  grp1  13553  grp1inv  13554  ring1  13936  psrval  14543  fnpsr  14544  psrbasg  14551  psrplusgg  14555  txlm  14866  struct2slots2dom  15752  structvtxval  15753  structiedg0val  15754  structgrssvtx  15756  structgrssiedg  15757  gropd  15761  edgopval  15773  edgstruct  15775  isuhgropm  15792  uhgrunop  15798  upgrop  15815  upgr0eop  15830  upgr1eopdc  15831  upgrunop  15833  umgrunop  15835