MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexeqdv Structured version   Unicode version

Theorem rexeqdv 3029
Description: Equality deduction for restricted existential quantifier. (Contributed by NM, 14-Jan-2007.)
Hypothesis
Ref Expression
raleq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
rexeqdv  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  B  ps )
)
Distinct variable groups:    x, A    x, B
Allowed substitution hints:    ph( x)    ps( x)

Proof of Theorem rexeqdv
StepHypRef Expression
1 raleq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 rexeq 3023 . 2  |-  ( A  =  B  ->  ( E. x  e.  A  ps 
<->  E. x  e.  B  ps ) )
31, 2syl 17 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  B  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437   E.wrex 2772
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-cleq 2414  df-clel 2417  df-nfc 2568  df-rex 2777
This theorem is referenced by:  rexeqbidv  3037  rexeqbidva  3039  fnunirn  6173  oarec  7274  fival  7935  marypha1lem  7956  marypha1  7957  wemapwe  8210  zornn0g  8942  scshwfzeqfzo  12927  supcvg  13913  zprod  13990  vdwlem6  14935  rami  14971  cshws0  15071  imasleval  15446  isssc  15724  fullestrcsetc  16035  fullsetcestrc  16050  ipodrsfi  16408  grppropd  16683  sylow1lem2  17250  sylow3lem1  17278  lsmass  17319  pj1fval  17343  efgrelexlema  17398  ablfacrplem  17697  pgpfac1lem2  17707  pgpfac1lem3  17709  pgpfac1lem4  17710  ablfac2  17721  dvdsrval  17872  dvdsrpropd  17923  znunit  19132  ellspd  19358  cnpfval  20248  cmpcov  20402  cmpsublem  20412  cmpsub  20413  tgcmp  20414  uncmp  20416  hauscmplem  20419  1stcfb  20458  2ndcctbss  20468  1stcelcls  20474  llyi  20487  nllyi  20488  cldllycmp  20508  ptrescn  20652  isufl  20926  fmid  20973  alexsublem  21057  alexsubb  21059  alexsubALTlem4  21063  alexsubALT  21064  cnextfres1  21081  tsmsf1o  21157  utopval  21245  imasf1oxms  21502  bndth  21984  ovolicc2  22474  ellimc2  22830  limcflf  22834  plyval  23145  aannenlem1  23282  aannenlem2  23283  ulm2  23338  ishpg  24799  nb3graprlem2  25178  fargshiftfo  25364  wwlkextsur  25457  erclwwlknsym  25552  erclwwlkntr  25553  hashecclwwlkn1  25560  usghashecclwwlk  25561  frgra2v  25725  isplig  25907  isgrp2d  25961  isgrpda  26023  pjhth  27044  pjhfval  27047  pjhtheu2  27067  iscref  28679  crefeq  28680  issros  29005  eulerpartlemgh  29219  ballotlemfc0  29333  ballotlemfcc  29334  ispcon  29954  br8  30403  br6  30404  br4  30405  wsuclem  30515  brsegle  30880  hilbert1.1  30926  limsucncmpi  31110  poimirlem24  31928  poimirlem25  31929  poimirlem27  31931  poimirlem28  31932  volsupnfl  31949  isdrngo2  32161  lcvfbr  32555  lkrlspeqN  32706  pointsetN  33275  dia1dim2  34599  dib1dim2  34705  diclspsn  34731  dih1dimatlem  34866  lcfrvalsnN  35078  mapdpglem3  35212  mapdpglem26  35235  mapdpglem27  35236  isnacs  35515  eldioph  35569  islssfg  35898  itgoval  35997  stoweidlem50  37851  stoweidlem57  37858  iccelpart  38617  dfnbgr3  39174  nb3grprlem2  39214  cplgrop  39260  cusgrexi  39263  lco0  39841
  Copyright terms: Public domain W3C validator