Theorem opexg 4368

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 3902	. 2 |- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
2		elex 2833	. . . . 5 |- ( A e. V -> A e. _V )
3		snexg 4321	. . . . 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 2833	. . . 4 |- ( B e. W -> B e. _V )
7		prexg 4349	. . . 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 4349	. . 3 |- ( ( { A } e. _V /\ { A , B } e. _V ) -> { { A } , { A , B } } e. _V )
10	5, 8, 9	syl2anc 415	. 2 |- ( ( A e. V /\ B e. W ) -> { { A } , { A , B } } e. _V )
11	1, 10	eqeltrd 2315	1 |- ( ( A e. V /\ B e. W ) -> <. A , B >. e. _V )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209   _Vcvv 2821   {csn 3709   {cpr 3710   <.cop 3712

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4249  ax-pow 4311  ax-pr 4346

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718

This theorem is used by:  opex  4369  otexg  4370  opeliunxp  4830  opbrop  4854  relsnopg  4879  opswapg  5274  elxp4  5275  elxp5  5276  resfunexg  5936  fliftel  5999  fliftel1  6000  oprabid  6117  ovexg  6119  ovssunirng  6120  eloprabga  6175  op1st  6380  op2nd  6381  ot1stg  6386  ot2ndg  6387  ot3rdgg  6388  elxp6  6403  mpofvex  6441  algrflem  6465  algrflemg  6466  mpoxopoveq  6511  brtposg  6525  tfr0dm  6593  tfrlemisucaccv  6596  tfrlemibxssdm  6598  tfrlemibfn  6599  tfrlemi14d  6604  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemres  6620  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemres  6633  mapsnend  7099  en2prd  7106  fnfi  7250  snopfsuppdc  7299  djulclb  7395  inl11  7405  1stinl  7414  2ndinl  7415  1stinr  7416  2ndinr  7417  mulpipq2  7738  enq0breq  7803  addvalex  8211  peano2nnnn  8220  axcnre  8248  frec2uzrdg  10859  frecuzrdg0  10863  frecuzrdgg  10866  frecuzrdg0t  10872  zfz1isolem1  11306  s1leng  11406  s111  11413  pfxclz  11465  eucalgval2  12847  crth  13022  phimullem  13023  ennnfonelemp1  13346  setsvala  13432  setsex  13433  setsfun  13436  setsfun0  13437  setsresg  13439  setscom  13441  strslfv  13446  strslfv3  13447  setsslid  13452  bassetsnn  13458  strle1g  13509  1strbas  13520  2strbasg  13523  2stropg  13524  2strbas1g  13526  2strop1g  13527  rngbaseg  13539  rngplusgg  13540  rngmulrg  13541  srngbased  13550  srngplusgd  13551  srngmulrd  13552  srnginvld  13553  lmodbased  13568  lmodplusgd  13569  lmodscad  13570  lmodvscad  13571  ipsbased  13580  ipsaddgd  13581  ipsmulrd  13582  ipsscad  13583  ipsvscad  13584  ipsipd  13585  topgrpbasd  13600  topgrpplusgd  13601  topgrptsetd  13602  imasex  13675  imasival  13676  imasbas  13677  imasplusg  13678  imasmulr  13679  imasaddfnlemg  13684  imasaddvallemg  13685  xpsfval  13718  intopsn  13736  mgm1  13739  sgrp1  13775  mnd1  13811  mnd1id  13812  grp1  13960  grp1inv  13961  prdsex  14221  prdsval  14222  xpsval  14250  ring1  14413  psrval  15099  fnpsr  15100  psrbasg  15114  psrplusgg  15118  txlm  15429  struct2slots2dom  16377  structvtxval  16378  structiedg0val  16379  structgrssvtx  16381  structgrssiedg  16382  gropd  16386  edgopval  16401  edgstruct  16403  isuhgropm  16420  uhgrunop  16426  upgrop  16443  upgr0eop  16461  upgr1eopdc  16462  upgr1een  16463  umgr1een  16464  upgrunop  16466  umgrunop  16468  isuspgropen  16503  isusgropen  16504  ausgrusgrben  16507  usgr0eop  16581  uspgr1eopdc  16582  usgr1eop  16584  uhgrspanop  16621  vtxdgop  16631  p1evtxdeqfilem  16650  p1evtxdeqfi  16651  p1evtxdp1fi  16652  eupthvdres  16814  eupth2lem3fi  16815  konigsbergumgr  16826