Theorem opexg 4213

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 3763	. 2 |- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
2		elex 2741	. . . . 5 |- ( A e. V -> A e. _V )
3		snexg 4170	. . . . 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 2741	. . . 4 |- ( B e. W -> B e. _V )
7		prexg 4196	. . . 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 4196	. . 3 |- ( ( { A } e. _V /\ { A , B } e. _V ) -> { { A } , { A , B } } e. _V )
10	5, 8, 9	syl2anc 409	. 2 |- ( ( A e. V /\ B e. W ) -> { { A } , { A , B } } e. _V )
11	1, 10	eqeltrd 2247	1 |- ( ( A e. V /\ B e. W ) -> <. A , B >. e. _V )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 2141   _Vcvv 2730   {csn 3583   {cpr 3584   <.cop 3586

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-pow 4160  ax-pr 4194

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592

This theorem is referenced by:  opex  4214  otexg  4215  opeliunxp  4666  opbrop  4690  relsnopg  4715  opswapg  5097  elxp4  5098  elxp5  5099  resfunexg  5717  fliftel  5772  fliftel1  5773  oprabid  5885  ovexg  5887  eloprabga  5940  op1st  6125  op2nd  6126  ot1stg  6131  ot2ndg  6132  ot3rdgg  6133  elxp6  6148  mpofvex  6182  algrflem  6208  algrflemg  6209  mpoxopoveq  6219  brtposg  6233  tfr0dm  6301  tfrlemisucaccv  6304  tfrlemibxssdm  6306  tfrlemibfn  6307  tfrlemi14d  6312  tfr1onlemsucaccv  6320  tfr1onlembxssdm  6322  tfr1onlembfn  6323  tfr1onlemres  6328  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllembfn  6336  tfrcllemres  6341  fnfi  6914  djulclb  7032  inl11  7042  1stinl  7051  2ndinl  7052  1stinr  7053  2ndinr  7054  mulpipq2  7333  enq0breq  7398  addvalex  7806  peano2nnnn  7815  axcnre  7843  frec2uzrdg  10365  frecuzrdg0  10369  frecuzrdgg  10372  frecuzrdg0t  10378  zfz1isolem1  10775  eucalgval2  12007  crth  12178  phimullem  12179  ennnfonelemp1  12361  setsvala  12447  setsex  12448  setsfun  12451  setsfun0  12452  setsresg  12454  setscom  12456  strslfv  12460  setsslid  12466  strle1g  12508  1strbas  12517  2strbasg  12519  2stropg  12520  2strbas1g  12522  2strop1g  12523  rngbaseg  12534  rngplusgg  12535  rngmulrg  12536  srngbased  12541  srngplusgd  12542  srngmulrd  12543  srnginvld  12544  lmodbased  12552  lmodplusgd  12553  lmodscad  12554  lmodvscad  12555  ipsbased  12560  ipsaddgd  12561  ipsmulrd  12562  ipsscad  12563  ipsvscad  12564  ipsipd  12565  topgrpbasd  12570  topgrpplusgd  12571  topgrptsetd  12572  intopsn  12621  mgm1  12624  sgrp1  12651  mnd1  12679  mnd1id  12680  txlm  13073