Theorem opexg 4320

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 3860	. 2 |- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
2		elex 2814	. . . . 5 |- ( A e. V -> A e. _V )
3		snexg 4274	. . . . 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 2814	. . . 4 |- ( B e. W -> B e. _V )
7		prexg 4301	. . . 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 4301	. . 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 2308	1 |- ( ( A e. V /\ B e. W ) -> <. A , B >. e. _V )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2202   _Vcvv 2802   {csn 3669   {cpr 3670   <.cop 3672

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678

This theorem is referenced by:  opex  4321  otexg  4322  opeliunxp  4781  opbrop  4805  relsnopg  4830  opswapg  5223  elxp4  5224  elxp5  5225  resfunexg  5875  fliftel  5934  fliftel1  5935  oprabid  6050  ovexg  6052  ovssunirng  6053  eloprabga  6108  op1st  6309  op2nd  6310  ot1stg  6315  ot2ndg  6316  ot3rdgg  6317  elxp6  6332  mpofvex  6370  algrflem  6394  algrflemg  6395  mpoxopoveq  6406  brtposg  6420  tfr0dm  6488  tfrlemisucaccv  6491  tfrlemibxssdm  6493  tfrlemibfn  6494  tfrlemi14d  6499  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfr1onlemres  6515  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemres  6528  en2prd  6992  fnfi  7135  djulclb  7254  inl11  7264  1stinl  7273  2ndinl  7274  1stinr  7275  2ndinr  7276  mulpipq2  7591  enq0breq  7656  addvalex  8064  peano2nnnn  8073  axcnre  8101  frec2uzrdg  10671  frecuzrdg0  10675  frecuzrdgg  10678  frecuzrdg0t  10684  zfz1isolem1  11104  s1leng  11201  s111  11208  pfxclz  11260  eucalgval2  12626  crth  12797  phimullem  12798  ennnfonelemp1  13028  setsvala  13114  setsex  13115  setsfun  13118  setsfun0  13119  setsresg  13121  setscom  13123  strslfv  13128  strslfv3  13129  setsslid  13134  bassetsnn  13140  strle1g  13190  1strbas  13201  2strbasg  13204  2stropg  13205  2strbas1g  13207  2strop1g  13208  rngbaseg  13220  rngplusgg  13221  rngmulrg  13222  srngbased  13231  srngplusgd  13232  srngmulrd  13233  srnginvld  13234  lmodbased  13249  lmodplusgd  13250  lmodscad  13251  lmodvscad  13252  ipsbased  13261  ipsaddgd  13262  ipsmulrd  13263  ipsscad  13264  ipsvscad  13265  ipsipd  13266  topgrpbasd  13281  topgrpplusgd  13282  topgrptsetd  13283  prdsex  13353  prdsval  13357  imasex  13389  imasival  13390  imasbas  13391  imasplusg  13392  imasmulr  13393  imasaddfnlemg  13398  imasaddvallemg  13399  xpsfval  13432  xpsval  13436  intopsn  13451  mgm1  13454  sgrp1  13495  mnd1  13539  mnd1id  13540  grp1  13690  grp1inv  13691  ring1  14074  psrval  14682  fnpsr  14683  psrbasg  14690  psrplusgg  14694  txlm  15005  struct2slots2dom  15891  structvtxval  15892  structiedg0val  15893  structgrssvtx  15895  structgrssiedg  15896  gropd  15900  edgopval  15915  edgstruct  15917  isuhgropm  15934  uhgrunop  15940  upgrop  15957  upgr0eop  15975  upgr1eopdc  15976  upgr1een  15977  umgr1een  15978  upgrunop  15980  umgrunop  15982  isuspgropen  16017  isusgropen  16018  ausgrusgrben  16021  usgr0eop  16095  uspgr1eopdc  16096  usgr1eop  16098  uhgrspanop  16135  vtxdgop  16145  p1evtxdeqfilem  16164  p1evtxdeqfi  16165  p1evtxdp1fi  16166