Theorem opexg 4273

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 3817	. 2 |- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
2		elex 2783	. . . . 5 |- ( A e. V -> A e. _V )
3		snexg 4229	. . . . 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 2783	. . . 4 |- ( B e. W -> B e. _V )
7		prexg 4256	. . . 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 4256	. . 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 2282	1 |- ( ( A e. V /\ B e. W ) -> <. A , B >. e. _V )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2176   _Vcvv 2772   {csn 3633   {cpr 3634   <.cop 3636

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4163  ax-pow 4219  ax-pr 4254

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642

This theorem is referenced by:  opex  4274  otexg  4275  opeliunxp  4731  opbrop  4755  relsnopg  4780  opswapg  5170  elxp4  5171  elxp5  5172  resfunexg  5807  fliftel  5864  fliftel1  5865  oprabid  5978  ovexg  5980  ovssunirng  5981  eloprabga  6034  op1st  6234  op2nd  6235  ot1stg  6240  ot2ndg  6241  ot3rdgg  6242  elxp6  6257  mpofvex  6293  algrflem  6317  algrflemg  6318  mpoxopoveq  6328  brtposg  6342  tfr0dm  6410  tfrlemisucaccv  6413  tfrlemibxssdm  6415  tfrlemibfn  6416  tfrlemi14d  6421  tfr1onlemsucaccv  6429  tfr1onlembxssdm  6431  tfr1onlembfn  6432  tfr1onlemres  6437  tfrcllemsucaccv  6442  tfrcllembxssdm  6444  tfrcllembfn  6445  tfrcllemres  6450  en2prd  6911  fnfi  7040  djulclb  7159  inl11  7169  1stinl  7178  2ndinl  7179  1stinr  7180  2ndinr  7181  mulpipq2  7486  enq0breq  7551  addvalex  7959  peano2nnnn  7968  axcnre  7996  frec2uzrdg  10556  frecuzrdg0  10560  frecuzrdgg  10563  frecuzrdg0t  10569  zfz1isolem1  10987  s1leng  11081  s111  11088  eucalgval2  12408  crth  12579  phimullem  12580  ennnfonelemp1  12810  setsvala  12896  setsex  12897  setsfun  12900  setsfun0  12901  setsresg  12903  setscom  12905  strslfv  12910  strslfv3  12911  setsslid  12916  strle1g  12971  1strbas  12982  2strbasg  12985  2stropg  12986  2strbas1g  12988  2strop1g  12989  rngbaseg  13001  rngplusgg  13002  rngmulrg  13003  srngbased  13012  srngplusgd  13013  srngmulrd  13014  srnginvld  13015  lmodbased  13030  lmodplusgd  13031  lmodscad  13032  lmodvscad  13033  ipsbased  13042  ipsaddgd  13043  ipsmulrd  13044  ipsscad  13045  ipsvscad  13046  ipsipd  13047  topgrpbasd  13062  topgrpplusgd  13063  topgrptsetd  13064  prdsex  13134  prdsval  13138  imasex  13170  imasival  13171  imasbas  13172  imasplusg  13173  imasmulr  13174  imasaddfnlemg  13179  imasaddvallemg  13180  xpsfval  13213  xpsval  13217  intopsn  13232  mgm1  13235  sgrp1  13276  mnd1  13320  mnd1id  13321  grp1  13471  grp1inv  13472  ring1  13854  psrval  14461  fnpsr  14462  psrbasg  14469  psrplusgg  14473  txlm  14784  struct2slots2dom  15668  structvtxval  15669  structiedg0val  15670  structgrssvtx  15672  structgrssiedg  15673  gropd  15677  edgopval  15689  edgstruct  15691