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

Theorem rexeqdv 2911
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 2905 . 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 set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652   E.wrex 2706
This theorem is referenced by:  rexeqbidv  2917  rexeqbidva  2919  fnunirn  5999  oarec  6805  fival  7417  marypha1lem  7438  marypha1  7439  wemapwe  7654  zornn0g  8385  supcvg  12635  vdwlem6  13354  rami  13383  imasleval  13766  isssc  14020  ipodrsfi  14589  grppropd  14823  sylow1lem2  15233  sylow3lem1  15261  lsmass  15302  pj1fval  15326  efgrelexlema  15381  ablfacrplem  15623  pgpfac1lem2  15633  pgpfac1lem3  15635  pgpfac1lem4  15636  ablfac2  15647  dvdsrval  15750  dvdsrpropd  15801  znunit  16844  cnpfval  17298  cmpcov  17452  cmpsublem  17462  cmpsub  17463  tgcmp  17464  uncmp  17466  hauscmplem  17469  bwth  17473  1stcfb  17508  2ndcctbss  17518  1stcelcls  17524  llyi  17537  nllyi  17538  cldllycmp  17558  ptrescn  17671  isufl  17945  fmid  17992  alexsublem  18075  alexsubb  18077  alexsubALTlem4  18081  alexsubALT  18082  cnextfres  18099  tsmsf1o  18174  utopval  18262  imasf1oxms  18519  bndth  18983  ovolicc2  19418  ellimc2  19764  limcflf  19768  plyval  20112  aannenlem1  20245  aannenlem2  20246  ulm2  20301  nb3graprlem2  21461  fargshiftfo  21625  isplig  21765  isgrp2d  21823  isgrpda  21885  pjhth  22895  pjhfval  22898  pjhtheu2  22918  ballotlemfc0  24750  ballotlemfcc  24751  ispcon  24910  zprod  25263  br8  25379  br6  25380  br4  25381  wsuclem  25576  brsegle  26042  hilbert1.1  26088  limsucncmpi  26195  volsupnfl  26251  isdrngo2  26574  isnacs  26758  eldioph  26816  islssfg  27145  ellspd  27231  itgoval  27343  stoweidlem50  27775  stoweidlem57  27782  frgra2v  28389  lcvfbr  29818  lkrlspeqN  29969  pointsetN  30538  dia1dim2  31860  dib1dim2  31966  diclspsn  31992  dih1dimatlem  32127  lcfrvalsnN  32339  mapdpglem3  32473  mapdpglem26  32496  mapdpglem27  32497
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rex 2711
  Copyright terms: Public domain W3C validator