Theorem opexg 4257

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 3802	. 2 |- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
2		elex 2771	. . . . 5 |- ( A e. V -> A e. _V )
3		snexg 4213	. . . . 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 2771	. . . 4 |- ( B e. W -> B e. _V )
7		prexg 4240	. . . 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 4240	. . 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 2270	1 |- ( ( A e. V /\ B e. W ) -> <. A , B >. e. _V )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2164   _Vcvv 2760   {csn 3618   {cpr 3619   <.cop 3621

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627

This theorem is referenced by:  opex  4258  otexg  4259  opeliunxp  4714  opbrop  4738  relsnopg  4763  opswapg  5152  elxp4  5153  elxp5  5154  resfunexg  5779  fliftel  5836  fliftel1  5837  oprabid  5950  ovexg  5952  eloprabga  6005  op1st  6199  op2nd  6200  ot1stg  6205  ot2ndg  6206  ot3rdgg  6207  elxp6  6222  mpofvex  6256  algrflem  6282  algrflemg  6283  mpoxopoveq  6293  brtposg  6307  tfr0dm  6375  tfrlemisucaccv  6378  tfrlemibxssdm  6380  tfrlemibfn  6381  tfrlemi14d  6386  tfr1onlemsucaccv  6394  tfr1onlembxssdm  6396  tfr1onlembfn  6397  tfr1onlemres  6402  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllembfn  6410  tfrcllemres  6415  fnfi  6995  djulclb  7114  inl11  7124  1stinl  7133  2ndinl  7134  1stinr  7135  2ndinr  7136  mulpipq2  7431  enq0breq  7496  addvalex  7904  peano2nnnn  7913  axcnre  7941  frec2uzrdg  10480  frecuzrdg0  10484  frecuzrdgg  10487  frecuzrdg0t  10493  zfz1isolem1  10911  eucalgval2  12191  crth  12362  phimullem  12363  ennnfonelemp1  12563  setsvala  12649  setsex  12650  setsfun  12653  setsfun0  12654  setsresg  12656  setscom  12658  strslfv  12663  setsslid  12669  strle1g  12724  1strbas  12735  2strbasg  12737  2stropg  12738  2strbas1g  12740  2strop1g  12741  rngbaseg  12753  rngplusgg  12754  rngmulrg  12755  srngbased  12764  srngplusgd  12765  srngmulrd  12766  srnginvld  12767  lmodbased  12782  lmodplusgd  12783  lmodscad  12784  lmodvscad  12785  ipsbased  12794  ipsaddgd  12795  ipsmulrd  12796  ipsscad  12797  ipsvscad  12798  ipsipd  12799  topgrpbasd  12814  topgrpplusgd  12815  topgrptsetd  12816  prdsex  12880  imasex  12888  imasival  12889  imasbas  12890  imasplusg  12891  imasmulr  12892  imasaddfnlemg  12897  imasaddvallemg  12898  xpsfval  12931  xpsval  12935  intopsn  12950  mgm1  12953  sgrp1  12994  mnd1  13027  mnd1id  13028  grp1  13178  grp1inv  13179  ring1  13555  psrval  14152  fnpsr  14153  psrbasg  14159  psrplusgg  14162  txlm  14447