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

Theorem rexeq 2897
Description: Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.)
Assertion
Ref Expression
rexeq  |-  ( A  =  B  ->  ( E. x  e.  A  ph  <->  E. x  e.  B  ph ) )
Distinct variable groups:    x, A    x, B
Allowed substitution hint:    ph( x)

Proof of Theorem rexeq
StepHypRef Expression
1 nfcv 2571 . 2  |-  F/_ x A
2 nfcv 2571 . 2  |-  F/_ x B
31, 2rexeqf 2893 1  |-  ( A  =  B  ->  ( E. x  e.  A  ph  <->  E. x  e.  B  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652   E.wrex 2698
This theorem is referenced by:  rexeqi  2901  rexeqdv  2903  rexeqbi1dv  2905  unieq  4016  exss  4418  qseq1  6946  1sdom  7303  pssnn  7319  indexfi  7406  supeq1  7442  bnd2  7809  dfac2  8003  cflem  8118  cflecard  8125  cfeq0  8128  cfsuc  8129  cfflb  8131  cofsmo  8141  elwina  8553  eltskg  8617  rankcf  8644  elnp  8856  elnpi  8857  genpv  8868  xrsupsslem  10877  xrinfmsslem  10878  xrsupss  10879  xrinfmss  10880  isdrs  14383  isipodrs  14579  neifval  17155  ishaus  17378  2ndc1stc  17506  1stcrest  17508  lly1stc  17551  tx1stc  17674  isust  18225  iscfilu  18310  met1stc  18543  iscfil  19210  isgrpo  21776  chne0  22988  pstmfval  24283  dya2iocuni  24625  nobndlem2  25640  nobndlem8  25646  altxpeq1  25810  altxpeq2  25811  elhf2  26108  isref  26350  islocfin  26367  cover2g  26407  indexdom  26427  istotbnd  26469  diophrex  26825  hbtlem1  27295  hbtlem7  27297  pmapglb2xN  30506  paddval  30532  elpadd0  30543
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 2416
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 2428  df-clel 2431  df-nfc 2560  df-rex 2703
  Copyright terms: Public domain W3C validator