Theorem opexg 4226

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 3775	. 2 |- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
2		elex 2748	. . . . 5 |- ( A e. V -> A e. _V )
3		snexg 4182	. . . . 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 2748	. . . 4 |- ( B e. W -> B e. _V )
7		prexg 4209	. . . 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 4209	. . 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 2254	1 |- ( ( A e. V /\ B e. W ) -> <. A , B >. e. _V )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2148   _Vcvv 2737   {csn 3592   {cpr 3593   <.cop 3595

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4119  ax-pow 4172  ax-pr 4207

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601

This theorem is referenced by:  opex  4227  otexg  4228  opeliunxp  4679  opbrop  4703  relsnopg  4728  opswapg  5112  elxp4  5113  elxp5  5114  resfunexg  5734  fliftel  5789  fliftel1  5790  oprabid  5902  ovexg  5904  eloprabga  5957  op1st  6142  op2nd  6143  ot1stg  6148  ot2ndg  6149  ot3rdgg  6150  elxp6  6165  mpofvex  6199  algrflem  6225  algrflemg  6226  mpoxopoveq  6236  brtposg  6250  tfr0dm  6318  tfrlemisucaccv  6321  tfrlemibxssdm  6323  tfrlemibfn  6324  tfrlemi14d  6329  tfr1onlemsucaccv  6337  tfr1onlembxssdm  6339  tfr1onlembfn  6340  tfr1onlemres  6345  tfrcllemsucaccv  6350  tfrcllembxssdm  6352  tfrcllembfn  6353  tfrcllemres  6358  fnfi  6931  djulclb  7049  inl11  7059  1stinl  7068  2ndinl  7069  1stinr  7070  2ndinr  7071  mulpipq2  7365  enq0breq  7430  addvalex  7838  peano2nnnn  7847  axcnre  7875  frec2uzrdg  10402  frecuzrdg0  10406  frecuzrdgg  10409  frecuzrdg0t  10415  zfz1isolem1  10811  eucalgval2  12043  crth  12214  phimullem  12215  ennnfonelemp1  12397  setsvala  12483  setsex  12484  setsfun  12487  setsfun0  12488  setsresg  12490  setscom  12492  strslfv  12497  setsslid  12503  strle1g  12555  1strbas  12566  2strbasg  12568  2stropg  12569  2strbas1g  12571  2strop1g  12572  rngbaseg  12584  rngplusgg  12585  rngmulrg  12586  srngbased  12595  srngplusgd  12596  srngmulrd  12597  srnginvld  12598  lmodbased  12613  lmodplusgd  12614  lmodscad  12615  lmodvscad  12616  ipsbased  12625  ipsaddgd  12626  ipsmulrd  12627  ipsscad  12628  ipsvscad  12629  ipsipd  12630  topgrpbasd  12642  topgrpplusgd  12643  topgrptsetd  12644  intopsn  12716  mgm1  12719  sgrp1  12746  mnd1  12775  mnd1id  12776  grp1  12904  grp1inv  12905  ring1  13136  txlm  13561