Theorem opexg 4314

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 3855	. 2 |- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
2		elex 2811	. . . . 5 |- ( A e. V -> A e. _V )
3		snexg 4268	. . . . 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 2811	. . . 4 |- ( B e. W -> B e. _V )
7		prexg 4295	. . . 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 4295	. . 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 2306	1 |- ( ( A e. V /\ B e. W ) -> <. A , B >. e. _V )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2200   _Vcvv 2799   {csn 3666   {cpr 3667   <.cop 3669

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675

This theorem is referenced by:  opex  4315  otexg  4316  opeliunxp  4774  opbrop  4798  relsnopg  4823  opswapg  5215  elxp4  5216  elxp5  5217  resfunexg  5860  fliftel  5917  fliftel1  5918  oprabid  6033  ovexg  6035  ovssunirng  6036  eloprabga  6091  op1st  6292  op2nd  6293  ot1stg  6298  ot2ndg  6299  ot3rdgg  6300  elxp6  6315  mpofvex  6351  algrflem  6375  algrflemg  6376  mpoxopoveq  6386  brtposg  6400  tfr0dm  6468  tfrlemisucaccv  6471  tfrlemibxssdm  6473  tfrlemibfn  6474  tfrlemi14d  6479  tfr1onlemsucaccv  6487  tfr1onlembxssdm  6489  tfr1onlembfn  6490  tfr1onlemres  6495  tfrcllemsucaccv  6500  tfrcllembxssdm  6502  tfrcllembfn  6503  tfrcllemres  6508  en2prd  6970  fnfi  7103  djulclb  7222  inl11  7232  1stinl  7241  2ndinl  7242  1stinr  7243  2ndinr  7244  mulpipq2  7558  enq0breq  7623  addvalex  8031  peano2nnnn  8040  axcnre  8068  frec2uzrdg  10631  frecuzrdg0  10635  frecuzrdgg  10638  frecuzrdg0t  10644  zfz1isolem1  11062  s1leng  11157  s111  11164  pfxclz  11211  eucalgval2  12575  crth  12746  phimullem  12747  ennnfonelemp1  12977  setsvala  13063  setsex  13064  setsfun  13067  setsfun0  13068  setsresg  13070  setscom  13072  strslfv  13077  strslfv3  13078  setsslid  13083  bassetsnn  13089  strle1g  13139  1strbas  13150  2strbasg  13153  2stropg  13154  2strbas1g  13156  2strop1g  13157  rngbaseg  13169  rngplusgg  13170  rngmulrg  13171  srngbased  13180  srngplusgd  13181  srngmulrd  13182  srnginvld  13183  lmodbased  13198  lmodplusgd  13199  lmodscad  13200  lmodvscad  13201  ipsbased  13210  ipsaddgd  13211  ipsmulrd  13212  ipsscad  13213  ipsvscad  13214  ipsipd  13215  topgrpbasd  13230  topgrpplusgd  13231  topgrptsetd  13232  prdsex  13302  prdsval  13306  imasex  13338  imasival  13339  imasbas  13340  imasplusg  13341  imasmulr  13342  imasaddfnlemg  13347  imasaddvallemg  13348  xpsfval  13381  xpsval  13385  intopsn  13400  mgm1  13403  sgrp1  13444  mnd1  13488  mnd1id  13489  grp1  13639  grp1inv  13640  ring1  14022  psrval  14630  fnpsr  14631  psrbasg  14638  psrplusgg  14642  txlm  14953  struct2slots2dom  15839  structvtxval  15840  structiedg0val  15841  structgrssvtx  15843  structgrssiedg  15844  gropd  15848  edgopval  15862  edgstruct  15864  isuhgropm  15881  uhgrunop  15887  upgrop  15904  upgr0eop  15922  upgr1eopdc  15923  upgrunop  15925  umgrunop  15927  isuspgropen  15962  isusgropen  15963  ausgrusgrben  15966