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

Theorem rexeq 2750
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 2432 . 2  |-  F/_ x A
2 nfcv 2432 . 2  |-  F/_ x B
31, 2rexeqf 2746 1  |-  ( A  =  B  ->  ( E. x  e.  A  ph  <->  E. x  e.  B  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632   E.wrex 2557
This theorem is referenced by:  rexeqi  2754  rexeqdv  2756  rexeqbi1dv  2758  unieq  3852  exss  4252  qseq1  6725  1sdom  7081  pssnn  7097  indexfi  7179  supeq1  7214  bnd2  7579  dfac2  7773  cflem  7888  cflecard  7895  cfeq0  7898  cfsuc  7899  cfflb  7901  cofsmo  7911  elwina  8324  eltskg  8388  rankcf  8415  elnp  8627  elnpi  8628  genpv  8639  xrsupsslem  10641  xrinfmsslem  10642  xrsupss  10643  xrinfmss  10644  isdrs  14084  isipodrs  14280  neifval  16852  ishaus  17066  2ndc1stc  17193  1stcrest  17195  lly1stc  17238  tx1stc  17360  met1stc  18083  iscfil  18707  isgrpo  20879  chne0  22089  nobndlem2  24418  nobndlem8  24424  altxpeq1  24579  altxpeq2  24580  elhf2  24877  ab2rexexg  25225  isdir2  25395  tcnvec  25793  vtarsu  25989  isibg2  26213  isibcg  26294  isref  26382  islocfin  26399  cover2g  26462  indexdom  26516  istotbnd  26596  diophrex  26958  hbtlem1  27430  hbtlem7  27432  stoweidlem50  27902  pmapglb2xN  30583  paddval  30609  elpadd0  30620
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562
  Copyright terms: Public domain W3C validator