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

Theorem rexeqdv 3047
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 3041 . 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 1383   E.wrex 2794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rex 2799
This theorem is referenced by:  rexeqbidv  3055  rexeqbidva  3057  fnunirn  6150  oarec  7213  fival  7874  marypha1lem  7895  marypha1  7896  wemapwe  8142  wemapweOLD  8143  zornn0g  8888  scshwfzeqfzo  12776  supcvg  13649  zprod  13726  vdwlem6  14486  rami  14515  cshws0  14568  imasleval  14920  isssc  15171  ipodrsfi  15772  grppropd  16047  sylow1lem2  16598  sylow3lem1  16626  lsmass  16667  pj1fval  16691  efgrelexlema  16746  ablfacrplem  17095  pgpfac1lem2  17105  pgpfac1lem3  17107  pgpfac1lem4  17108  ablfac2  17119  dvdsrval  17273  dvdsrpropd  17324  znunit  18580  ellspd  18814  ellspdOLD  18815  cnpfval  19713  cmpcov  19867  cmpsublem  19877  cmpsub  19878  tgcmp  19879  uncmp  19881  hauscmplem  19884  bwthOLD  19889  1stcfb  19924  2ndcctbss  19934  1stcelcls  19940  llyi  19953  nllyi  19954  cldllycmp  19974  ptrescn  20118  isufl  20392  fmid  20439  alexsublem  20522  alexsubb  20524  alexsubALTlem4  20528  alexsubALT  20529  cnextfres  20546  tsmsf1o  20625  utopval  20713  imasf1oxms  20970  bndth  21436  ovolicc2  21911  ellimc2  22259  limcflf  22263  plyval  22568  aannenlem1  22702  aannenlem2  22703  ulm2  22758  ishpg  24106  nb3graprlem2  24430  fargshiftfo  24616  wwlkextsur  24709  erclwwlknsym  24804  erclwwlkntr  24805  hashecclwwlkn1  24812  usghashecclwwlk  24813  frgra2v  24977  isplig  25157  isgrp2d  25215  isgrpda  25277  pjhth  26289  pjhfval  26292  pjhtheu2  26312  iscref  27825  crefeq  27826  eulerpartlemgh  28295  ballotlemfc0  28409  ballotlemfcc  28410  ispcon  28646  br8  29161  br6  29162  br4  29163  wsuclem  29357  brsegle  29734  hilbert1.1  29780  limsucncmpi  29886  volsupnfl  30035  isdrngo2  30337  isnacs  30612  eldioph  30667  islssfg  30992  itgoval  31086  stoweidlem50  31786  stoweidlem57  31793  fullestrcsetc  32623  fullsetcestrc  32638  lco0  32898  lcvfbr  34620  lkrlspeqN  34771  pointsetN  35340  dia1dim2  36664  dib1dim2  36770  diclspsn  36796  dih1dimatlem  36931  lcfrvalsnN  37143  mapdpglem3  37277  mapdpglem26  37300  mapdpglem27  37301
  Copyright terms: Public domain W3C validator