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

Theorem rexeq 3052
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 2622 . 2  |-  F/_ x A
2 nfcv 2622 . 2  |-  F/_ x B
31, 2rexeqf 3048 1  |-  ( A  =  B  ->  ( E. x  e.  A  ph  <->  E. x  e.  B  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1374   E.wrex 2808
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-cleq 2452  df-clel 2455  df-nfc 2610  df-rex 2813
This theorem is referenced by:  rexeqi  3056  rexeqdv  3058  rexeqbi1dv  3060  unieq  4246  exss  4703  qseq1  7351  1sdom  7712  pssnn  7728  indexfi  7817  supeq1  7894  bnd2  8300  dfac2  8500  cflem  8615  cflecard  8622  cfeq0  8625  cfsuc  8626  cfflb  8628  cofsmo  8638  elwina  9053  eltskg  9117  rankcf  9144  elnp  9354  elnpi  9355  genpv  9366  xrsupsslem  11487  xrinfmsslem  11488  xrsupss  11489  xrinfmss  11490  isdrs  15410  isipodrs  15637  neifval  19359  ishaus  19582  2ndc1stc  19711  1stcrest  19713  lly1stc  19756  tx1stc  19879  isust  20434  iscfilu  20519  met1stc  20752  iscfil  21432  isgrpo  24860  chne0  26074  pstmfval  27497  dya2iocuni  27880  nobndlem2  29016  nobndlem8  29022  altxpeq1  29186  altxpeq2  29187  elhf2  29395  isref  29738  islocfin  29755  cover2g  29795  indexdom  29815  istotbnd  29855  diophrex  30300  hbtlem1  30665  hbtlem7  30667  fourierdlem70  31432  fourierdlem80  31442  bj-sngleq  33481  pmapglb2xN  34443  paddval  34469  elpadd0  34480
  Copyright terms: Public domain W3C validator