Theorem opexg 4145

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 3698	. 2 |- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
2		elex 2692	. . . . 5 |- ( A e. V -> A e. _V )
3		snexg 4103	. . . . 5 |- ( A e. _V -> { A } e. _V )
4	2, 3	syl 14	. . . 4 |- ( A e. V -> { A } e. _V )
5	4	adantr 274	. . 3 |- ( ( A e. V /\ B e. W ) -> { A } e. _V )
6		elex 2692	. . . 4 |- ( B e. W -> B e. _V )
7		prexg 4128	. . . 4 |- ( ( A e. _V /\ B e. _V ) -> { A , B } e. _V )
8	2, 6, 7	syl2an 287	. . 3 |- ( ( A e. V /\ B e. W ) -> { A , B } e. _V )
9		prexg 4128	. . 3 |- ( ( { A } e. _V /\ { A , B } e. _V ) -> { { A } , { A , B } } e. _V )
10	5, 8, 9	syl2anc 408	. 2 |- ( ( A e. V /\ B e. W ) -> { { A } , { A , B } } e. _V )
11	1, 10	eqeltrd 2214	1 |- ( ( A e. V /\ B e. W ) -> <. A , B >. e. _V )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1480   _Vcvv 2681   {csn 3522   {cpr 3523   <.cop 3525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-sep 4041  ax-pow 4093  ax-pr 4126

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-v 2683  df-un 3070  df-in 3072  df-ss 3079  df-pw 3507  df-sn 3528  df-pr 3529  df-op 3531

This theorem is referenced by:  opex  4146  otexg  4147  opeliunxp  4589  opbrop  4613  relsnopg  4638  opswapg  5020  elxp4  5021  elxp5  5022  resfunexg  5634  fliftel  5687  fliftel1  5688  oprabid  5796  ovexg  5798  eloprabga  5851  op1st  6037  op2nd  6038  ot1stg  6043  ot2ndg  6044  ot3rdgg  6045  elxp6  6060  mpofvex  6094  algrflem  6119  algrflemg  6120  mpoxopoveq  6130  brtposg  6144  tfr0dm  6212  tfrlemisucaccv  6215  tfrlemibxssdm  6217  tfrlemibfn  6218  tfrlemi14d  6223  tfr1onlemsucaccv  6231  tfr1onlembxssdm  6233  tfr1onlembfn  6234  tfr1onlemres  6239  tfrcllemsucaccv  6244  tfrcllembxssdm  6246  tfrcllembfn  6247  tfrcllemres  6252  fnfi  6818  djulclb  6933  inl11  6943  1stinl  6952  2ndinl  6953  1stinr  6954  2ndinr  6955  mulpipq2  7172  enq0breq  7237  addvalex  7645  peano2nnnn  7654  axcnre  7682  frec2uzrdg  10175  frecuzrdg0  10179  frecuzrdgg  10182  frecuzrdg0t  10188  zfz1isolem1  10576  eucalgval2  11723  crth  11889  phimullem  11890  ennnfonelemp1  11908  setsvala  11979  setsex  11980  setsfun  11983  setsfun0  11984  setsresg  11986  setscom  11988  strslfv  11992  setsslid  11998  strle1g  12038  1strbas  12047  2strbasg  12049  2stropg  12050  2strbas1g  12052  2strop1g  12053  rngbaseg  12064  rngplusgg  12065  rngmulrg  12066  srngbased  12071  srngplusgd  12072  srngmulrd  12073  srnginvld  12074  lmodbased  12082  lmodplusgd  12083  lmodscad  12084  lmodvscad  12085  ipsbased  12090  ipsaddgd  12091  ipsmulrd  12092  ipsscad  12093  ipsvscad  12094  ipsipd  12095  topgrpbasd  12100  topgrpplusgd  12101  topgrptsetd  12102  txlm  12437