Theorem opexg 4108

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 3667	. 2 |- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
2		elex 2666	. . . . 5 |- ( A e. V -> A e. _V )
3		snexg 4066	. . . . 5 |- ( A e. _V -> { A } e. _V )
4	2, 3	syl 14	. . . 4 |- ( A e. V -> { A } e. _V )
5	4	adantr 272	. . 3 |- ( ( A e. V /\ B e. W ) -> { A } e. _V )
6		elex 2666	. . . 4 |- ( B e. W -> B e. _V )
7		prexg 4091	. . . 4 |- ( ( A e. _V /\ B e. _V ) -> { A , B } e. _V )
8	2, 6, 7	syl2an 285	. . 3 |- ( ( A e. V /\ B e. W ) -> { A , B } e. _V )
9		prexg 4091	. . 3 |- ( ( { A } e. _V /\ { A , B } e. _V ) -> { { A } , { A , B } } e. _V )
10	5, 8, 9	syl2anc 406	. 2 |- ( ( A e. V /\ B e. W ) -> { { A } , { A , B } } e. _V )
11	1, 10	eqeltrd 2189	1 |- ( ( A e. V /\ B e. W ) -> <. A , B >. e. _V )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1461   _Vcvv 2655   {csn 3491   {cpr 3492   <.cop 3494

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-pow 4056  ax-pr 4089

This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-v 2657  df-un 3039  df-in 3041  df-ss 3048  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500

This theorem is referenced by:  opex  4109  otexg  4110  opeliunxp  4552  opbrop  4576  relsnopg  4601  opswapg  4981  elxp4  4982  elxp5  4983  resfunexg  5593  fliftel  5646  fliftel1  5647  oprabid  5755  ovexg  5757  eloprabga  5810  op1st  5996  op2nd  5997  ot1stg  6002  ot2ndg  6003  ot3rdgg  6004  elxp6  6019  mpofvex  6053  algrflem  6078  algrflemg  6079  mpoxopoveq  6089  brtposg  6103  tfr0dm  6171  tfrlemisucaccv  6174  tfrlemibxssdm  6176  tfrlemibfn  6177  tfrlemi14d  6182  tfr1onlemsucaccv  6190  tfr1onlembxssdm  6192  tfr1onlembfn  6193  tfr1onlemres  6198  tfrcllemsucaccv  6203  tfrcllembxssdm  6205  tfrcllembfn  6206  tfrcllemres  6211  fnfi  6775  djulclb  6890  inl11  6900  1stinl  6909  2ndinl  6910  1stinr  6911  2ndinr  6912  mulpipq2  7121  enq0breq  7186  addvalex  7573  peano2nnnn  7582  axcnre  7610  frec2uzrdg  10069  frecuzrdg0  10073  frecuzrdgg  10076  frecuzrdg0t  10082  zfz1isolem1  10470  eucalgval2  11574  crth  11739  phimullem  11740  ennnfonelemp1  11758  setsvala  11827  setsex  11828  setsfun  11831  setsfun0  11832  setsresg  11834  setscom  11836  strslfv  11840  setsslid  11846  strle1g  11886  1strbas  11895  2strbasg  11897  2stropg  11898  2strbas1g  11900  2strop1g  11901  rngbaseg  11912  rngplusgg  11913  rngmulrg  11914  srngbased  11919  srngplusgd  11920  srngmulrd  11921  srnginvld  11922  lmodbased  11930  lmodplusgd  11931  lmodscad  11932  lmodvscad  11933  ipsbased  11938  ipsaddgd  11939  ipsmulrd  11940  ipsscad  11941  ipsvscad  11942  ipsipd  11943  topgrpbasd  11948  topgrpplusgd  11949  topgrptsetd  11950  txlm  12284