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

Theorem rexeq 2737
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 2419 . 2  |-  F/_ x A
2 nfcv 2419 . 2  |-  F/_ x B
31, 2rexeqf 2733 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 1623   E.wrex 2544
This theorem is referenced by:  rexeqi  2741  rexeqdv  2743  rexeqbi1dv  2745  unieq  3836  exss  4236  qseq1  6709  1sdom  7065  pssnn  7081  indexfi  7163  supeq1  7198  bnd2  7563  dfac2  7757  cflem  7872  cflecard  7879  cfeq0  7882  cfsuc  7883  cfflb  7885  cofsmo  7895  elwina  8308  eltskg  8372  rankcf  8399  elnp  8611  elnpi  8612  genpv  8623  xrsupsslem  10625  xrinfmsslem  10626  xrsupss  10627  xrinfmss  10628  isdrs  14068  isipodrs  14264  neifval  16836  ishaus  17050  2ndc1stc  17177  1stcrest  17179  lly1stc  17222  tx1stc  17344  met1stc  18067  iscfil  18691  isgrpo  20863  chne0  22073  nobndlem2  24347  nobndlem8  24353  altxpeq1  24507  altxpeq2  24508  elhf2  24805  ab2rexexg  25122  isdir2  25292  tcnvec  25690  vtarsu  25886  isibg2  26110  isibcg  26191  isref  26279  islocfin  26296  cover2g  26359  indexdom  26413  istotbnd  26493  diophrex  26855  hbtlem1  27327  hbtlem7  27329  stoweidlem50  27799  pmapglb2xN  29961  paddval  29987  elpadd0  29998
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549
  Copyright terms: Public domain W3C validator