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

Theorem rexeqdv 2986
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 2980 . 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 1399   E.wrex 2733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rex 2738
This theorem is referenced by:  rexeqbidv  2994  rexeqbidva  2996  fnunirn  6066  oarec  7129  fival  7787  marypha1lem  7808  marypha1  7809  wemapwe  8052  wemapweOLD  8053  zornn0g  8798  scshwfzeqfzo  12705  supcvg  13669  zprod  13746  vdwlem6  14506  rami  14535  cshws0  14588  imasleval  14948  isssc  15226  fullestrcsetc  15537  fullsetcestrc  15552  ipodrsfi  15910  grppropd  16185  sylow1lem2  16736  sylow3lem1  16764  lsmass  16805  pj1fval  16829  efgrelexlema  16884  ablfacrplem  17229  pgpfac1lem2  17239  pgpfac1lem3  17241  pgpfac1lem4  17242  ablfac2  17253  dvdsrval  17407  dvdsrpropd  17458  znunit  18693  ellspd  18922  cnpfval  19821  cmpcov  19975  cmpsublem  19985  cmpsub  19986  tgcmp  19987  uncmp  19989  hauscmplem  19992  1stcfb  20031  2ndcctbss  20041  1stcelcls  20047  llyi  20060  nllyi  20061  cldllycmp  20081  ptrescn  20225  isufl  20499  fmid  20546  alexsublem  20629  alexsubb  20631  alexsubALTlem4  20635  alexsubALT  20636  cnextfres  20653  tsmsf1o  20732  utopval  20820  imasf1oxms  21077  bndth  21543  ovolicc2  22018  ellimc2  22366  limcflf  22370  plyval  22675  aannenlem1  22809  aannenlem2  22810  ulm2  22865  ishpg  24248  nb3graprlem2  24573  fargshiftfo  24759  wwlkextsur  24852  erclwwlknsym  24947  erclwwlkntr  24948  hashecclwwlkn1  24955  usghashecclwwlk  24956  frgra2v  25120  isplig  25300  isgrp2d  25354  isgrpda  25416  pjhth  26428  pjhfval  26431  pjhtheu2  26451  iscref  28001  crefeq  28002  eulerpartlemgh  28500  ballotlemfc0  28614  ballotlemfcc  28615  ispcon  28857  br8  29351  br6  29352  br4  29353  wsuclem  29546  brsegle  29911  hilbert1.1  29957  limsucncmpi  30063  volsupnfl  30224  isdrngo2  30527  isnacs  30802  eldioph  30856  islssfg  31182  itgoval  31278  stoweidlem50  31998  stoweidlem57  32005  lco0  33228  lcvfbr  35158  lkrlspeqN  35309  pointsetN  35878  dia1dim2  37202  dib1dim2  37308  diclspsn  37334  dih1dimatlem  37469  lcfrvalsnN  37681  mapdpglem3  37815  mapdpglem26  37838  mapdpglem27  37839
  Copyright terms: Public domain W3C validator