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

Theorem rexeqdv 3060
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 3054 . 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 1374   E.wrex 2810
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-cleq 2454  df-clel 2457  df-nfc 2612  df-rex 2815
This theorem is referenced by:  rexeqbidv  3068  rexeqbidva  3070  fnunirn  6146  oarec  7203  fival  7863  marypha1lem  7884  marypha1  7885  wemapwe  8130  wemapweOLD  8131  zornn0g  8876  scshwfzeqfzo  12746  supcvg  13621  vdwlem6  14354  rami  14383  cshws0  14435  imasleval  14787  isssc  15041  ipodrsfi  15641  grppropd  15864  sylow1lem2  16410  sylow3lem1  16438  lsmass  16479  pj1fval  16503  efgrelexlema  16558  ablfacrplem  16901  pgpfac1lem2  16911  pgpfac1lem3  16913  pgpfac1lem4  16914  ablfac2  16925  dvdsrval  17073  dvdsrpropd  17124  znunit  18364  ellspd  18598  ellspdOLD  18599  cnpfval  19496  cmpcov  19650  cmpsublem  19660  cmpsub  19661  tgcmp  19662  uncmp  19664  hauscmplem  19667  bwthOLD  19672  1stcfb  19707  2ndcctbss  19717  1stcelcls  19723  llyi  19736  nllyi  19737  cldllycmp  19757  ptrescn  19870  isufl  20144  fmid  20191  alexsublem  20274  alexsubb  20276  alexsubALTlem4  20280  alexsubALT  20281  cnextfres  20298  tsmsf1o  20377  utopval  20465  imasf1oxms  20722  bndth  21188  ovolicc2  21663  ellimc2  22011  limcflf  22015  plyval  22320  aannenlem1  22453  aannenlem2  22454  ulm2  22509  nb3graprlem2  24116  fargshiftfo  24302  wwlkextsur  24395  erclwwlknsym  24490  erclwwlkntr  24491  hashecclwwlkn1  24498  usghashecclwwlk  24499  frgra2v  24663  isplig  24843  isgrp2d  24901  isgrpda  24963  pjhth  25975  pjhfval  25978  pjhtheu2  25998  eulerpartlemgh  27945  ballotlemfc0  28059  ballotlemfcc  28060  ispcon  28296  zprod  28634  br8  28750  br6  28751  br4  28752  wsuclem  28946  brsegle  29323  hilbert1.1  29369  limsucncmpi  29475  volsupnfl  29625  isdrngo2  29953  isnacs  30229  eldioph  30284  islssfg  30611  itgoval  30706  stoweidlem50  31307  stoweidlem57  31314  lco0  31978  lcvfbr  33694  lkrlspeqN  33845  pointsetN  34414  dia1dim2  35736  dib1dim2  35842  diclspsn  35868  dih1dimatlem  36003  lcfrvalsnN  36215  mapdpglem3  36349  mapdpglem26  36372  mapdpglem27  36373
  Copyright terms: Public domain W3C validator