Theorem opexg 4326

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 3865	. 2 |- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
2		elex 2815	. . . . 5 |- ( A e. V -> A e. _V )
3		snexg 4280	. . . . 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 2815	. . . 4 |- ( B e. W -> B e. _V )
7		prexg 4307	. . . 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 4307	. . 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 2308	1 |- ( ( A e. V /\ B e. W ) -> <. A , B >. e. _V )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2202   _Vcvv 2803   {csn 3673   {cpr 3674   <.cop 3676

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682

This theorem is referenced by:  opex  4327  otexg  4328  opeliunxp  4787  opbrop  4811  relsnopg  4836  opswapg  5230  elxp4  5231  elxp5  5232  resfunexg  5883  fliftel  5944  fliftel1  5945  oprabid  6060  ovexg  6062  ovssunirng  6063  eloprabga  6118  op1st  6318  op2nd  6319  ot1stg  6324  ot2ndg  6325  ot3rdgg  6326  elxp6  6341  mpofvex  6379  algrflem  6403  algrflemg  6404  mpoxopoveq  6449  brtposg  6463  tfr0dm  6531  tfrlemisucaccv  6534  tfrlemibxssdm  6536  tfrlemibfn  6537  tfrlemi14d  6542  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfr1onlemres  6558  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemres  6571  en2prd  7035  fnfi  7178  snopfsuppdc  7224  djulclb  7314  inl11  7324  1stinl  7333  2ndinl  7334  1stinr  7335  2ndinr  7336  mulpipq2  7651  enq0breq  7716  addvalex  8124  peano2nnnn  8133  axcnre  8161  frec2uzrdg  10734  frecuzrdg0  10738  frecuzrdgg  10741  frecuzrdg0t  10747  zfz1isolem1  11167  s1leng  11267  s111  11274  pfxclz  11326  eucalgval2  12705  crth  12876  phimullem  12877  ennnfonelemp1  13107  setsvala  13193  setsex  13194  setsfun  13197  setsfun0  13198  setsresg  13200  setscom  13202  strslfv  13207  strslfv3  13208  setsslid  13213  bassetsnn  13219  strle1g  13269  1strbas  13280  2strbasg  13283  2stropg  13284  2strbas1g  13286  2strop1g  13287  rngbaseg  13299  rngplusgg  13300  rngmulrg  13301  srngbased  13310  srngplusgd  13311  srngmulrd  13312  srnginvld  13313  lmodbased  13328  lmodplusgd  13329  lmodscad  13330  lmodvscad  13331  ipsbased  13340  ipsaddgd  13341  ipsmulrd  13342  ipsscad  13343  ipsvscad  13344  ipsipd  13345  topgrpbasd  13360  topgrpplusgd  13361  topgrptsetd  13362  prdsex  13432  prdsval  13436  imasex  13468  imasival  13469  imasbas  13470  imasplusg  13471  imasmulr  13472  imasaddfnlemg  13477  imasaddvallemg  13478  xpsfval  13511  xpsval  13515  intopsn  13530  mgm1  13533  sgrp1  13574  mnd1  13618  mnd1id  13619  grp1  13769  grp1inv  13770  ring1  14153  psrval  14762  fnpsr  14763  psrbasg  14775  psrplusgg  14779  txlm  15090  struct2slots2dom  15979  structvtxval  15980  structiedg0val  15981  structgrssvtx  15983  structgrssiedg  15984  gropd  15988  edgopval  16003  edgstruct  16005  isuhgropm  16022  uhgrunop  16028  upgrop  16045  upgr0eop  16063  upgr1eopdc  16064  upgr1een  16065  umgr1een  16066  upgrunop  16068  umgrunop  16070  isuspgropen  16105  isusgropen  16106  ausgrusgrben  16109  usgr0eop  16183  uspgr1eopdc  16184  usgr1eop  16186  uhgrspanop  16223  vtxdgop  16233  p1evtxdeqfilem  16252  p1evtxdeqfi  16253  p1evtxdp1fi  16254  eupthvdres  16416  eupth2lem3fi  16417  konigsbergumgr  16428