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

Theorem rexeqdv 2945
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 2939 . 2  |-  ( A  =  B  ->  ( E. x  e.  A  ps 
<->  E. x  e.  B  ps ) )
31, 2syl 16 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  B  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369   E.wrex 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rex 2742
This theorem is referenced by:  rexeqbidv  2953  rexeqbidva  2955  fnunirn  5991  oarec  7022  fival  7683  marypha1lem  7704  marypha1  7705  wemapwe  7949  wemapweOLD  7950  zornn0g  8695  supcvg  13339  vdwlem6  14068  rami  14097  cshws0  14149  imasleval  14500  isssc  14754  ipodrsfi  15354  grppropd  15577  sylow1lem2  16119  sylow3lem1  16147  lsmass  16188  pj1fval  16212  efgrelexlema  16267  ablfacrplem  16588  pgpfac1lem2  16598  pgpfac1lem3  16600  pgpfac1lem4  16601  ablfac2  16612  dvdsrval  16759  dvdsrpropd  16810  znunit  18018  ellspd  18252  ellspdOLD  18253  cnpfval  18860  cmpcov  19014  cmpsublem  19024  cmpsub  19025  tgcmp  19026  uncmp  19028  hauscmplem  19031  bwthOLD  19036  1stcfb  19071  2ndcctbss  19081  1stcelcls  19087  llyi  19100  nllyi  19101  cldllycmp  19121  ptrescn  19234  isufl  19508  fmid  19555  alexsublem  19638  alexsubb  19640  alexsubALTlem4  19644  alexsubALT  19645  cnextfres  19662  tsmsf1o  19741  utopval  19829  imasf1oxms  20086  bndth  20552  ovolicc2  21027  ellimc2  21374  limcflf  21378  plyval  21683  aannenlem1  21816  aannenlem2  21817  ulm2  21872  nb3graprlem2  23382  fargshiftfo  23546  isplig  23686  isgrp2d  23744  isgrpda  23806  pjhth  24818  pjhfval  24821  pjhtheu2  24841  eulerpartlemgh  26783  ballotlemfc0  26897  ballotlemfcc  26898  ispcon  27134  zprod  27472  br8  27588  br6  27589  br4  27590  wsuclem  27784  brsegle  28161  hilbert1.1  28207  limsucncmpi  28313  volsupnfl  28462  isdrngo2  28790  isnacs  29066  eldioph  29122  islssfg  29449  itgoval  29544  stoweidlem50  29871  stoweidlem57  29878  wwlkextsur  30389  scshwfzeqfzo  30518  erclwwlknsym  30526  erclwwlkntr  30527  hashecclwwlkn1  30534  usghashecclwwlk  30535  frgra2v  30617  lco0  30958  lcvfbr  32761  lkrlspeqN  32912  pointsetN  33481  dia1dim2  34803  dib1dim2  34909  diclspsn  34935  dih1dimatlem  35070  lcfrvalsnN  35282  mapdpglem3  35416  mapdpglem26  35439  mapdpglem27  35440
  Copyright terms: Public domain W3C validator