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

Theorem rexeq 2988
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 2592 . 2  |-  F/_ x A
2 nfcv 2592 . 2  |-  F/_ x B
31, 2rexeqf 2984 1  |-  ( A  =  B  ->  ( E. x  e.  A  ph  <->  E. x  e.  B  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    = wceq 1444   E.wrex 2738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-cleq 2444  df-clel 2447  df-nfc 2581  df-rex 2743
This theorem is referenced by:  rexeqi  2992  rexeqdv  2994  rexeqbi1dv  2996  unieq  4206  exss  4663  qseq1  7413  1sdom  7775  pssnn  7790  indexfi  7882  supeq1  7959  bnd2  8364  dfac2  8561  cflem  8676  cflecard  8683  cfeq0  8686  cfsuc  8687  cfflb  8689  cofsmo  8699  elwina  9111  eltskg  9175  rankcf  9202  elnp  9412  elnpi  9413  genpv  9424  xrsupsslem  11592  xrinfmsslem  11593  xrsupss  11594  xrinfmss  11595  hashge2el2difr  12638  isdrs  16179  isipodrs  16407  neifval  20115  ishaus  20338  2ndc1stc  20466  1stcrest  20468  lly1stc  20511  isref  20524  islocfin  20532  tx1stc  20665  isust  21218  iscfilu  21303  met1stc  21536  iscfil  22235  isgrpo  25924  chne0  27147  pstmfval  28699  dya2iocuni  29105  nobndlem2  30582  nobndlem8  30588  altxpeq1  30740  altxpeq2  30741  elhf2  30942  bj-sngleq  31561  cover2g  32041  indexdom  32061  istotbnd  32101  pmapglb2xN  33337  paddval  33363  elpadd0  33374  diophrex  35618  hbtlem1  35982  hbtlem7  35984
  Copyright terms: Public domain W3C validator