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

Theorem rexeqdv 2819
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 2813 . 2  |-  ( A  =  B  ->  ( E. x  e.  A  ps 
<->  E. x  e.  B  ps ) )
31, 2syl 15 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  B  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1642   E.wrex 2620
This theorem is referenced by:  rexeqbidv  2825  rexeqbidva  2827  fnunirn  5865  oarec  6647  fival  7256  marypha1lem  7276  marypha1  7277  wemapwe  7490  zornn0g  8222  supcvg  12411  vdwlem6  13130  rami  13159  imasleval  13542  isssc  13796  ipodrsfi  14365  grppropd  14599  sylow1lem2  15009  sylow3lem1  15037  lsmass  15078  pj1fval  15102  efgrelexlema  15157  ablfacrplem  15399  pgpfac1lem2  15409  pgpfac1lem3  15411  pgpfac1lem4  15412  ablfac2  15423  dvdsrval  15526  dvdsrpropd  15577  znunit  16623  cnpfval  17070  cmpcov  17222  cmpsublem  17232  cmpsub  17233  tgcmp  17234  uncmp  17236  hauscmplem  17239  1stcfb  17277  2ndcctbss  17287  1stcelcls  17293  llyi  17306  nllyi  17307  cldllycmp  17327  ptrescn  17439  isufl  17710  fmid  17757  alexsublem  17840  alexsubb  17842  alexsubALTlem4  17846  alexsubALT  17847  tsmsf1o  17929  imasf1oxms  18137  bndth  18560  ovolicc2  18985  ellimc2  19331  limcflf  19335  plyval  19679  aannenlem1  19812  aannenlem2  19813  ulm2  19868  isplig  20956  isgrp2d  21014  isgrpda  21076  pjhth  22086  pjhfval  22089  pjhtheu2  22109  utopval  23536  ballotlemfc0  23999  ballotlemfcc  24000  ispcon  24158  zprod  24564  br8  24671  br6  24672  br4  24673  brsegle  25290  hilbert1.1  25336  limsucncmpi  25443  volsupnfl  25491  isdrngo2  25912  isnacs  26102  eldioph  26160  islssfg  26491  ellspd  26577  itgoval  26689  nb3graprlem2  27615  fargshiftfo  27761  frgra2v  27832  lcvfbr  29279  lkrlspeqN  29430  pointsetN  29999  dia1dim2  31321  dib1dim2  31427  diclspsn  31453  dih1dimatlem  31588  lcfrvalsnN  31800  mapdpglem3  31934  mapdpglem26  31957  mapdpglem27  31958
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-cleq 2351  df-clel 2354  df-nfc 2483  df-rex 2625
  Copyright terms: Public domain W3C validator