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

Theorem rexeq 2974
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 2612 . 2  |-  F/_ x A
2 nfcv 2612 . 2  |-  F/_ x B
31, 2rexeqf 2970 1  |-  ( A  =  B  ->  ( E. x  e.  A  ph  <->  E. x  e.  B  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1452   E.wrex 2757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rex 2762
This theorem is referenced by:  rexeqi  2978  rexeqdv  2980  rexeqbi1dv  2982  unieq  4198  exss  4663  qseq1  7431  1sdom  7793  pssnn  7808  indexfi  7900  supeq1  7977  bnd2  8382  dfac2  8579  cflem  8694  cflecard  8701  cfeq0  8704  cfsuc  8705  cfflb  8707  cofsmo  8717  elwina  9129  eltskg  9193  rankcf  9220  elnp  9430  elnpi  9431  genpv  9442  xrsupsslem  11617  xrinfmsslem  11618  xrsupss  11619  xrinfmss  11620  hashge2el2difr  12679  isdrs  16257  isipodrs  16485  neifval  20192  ishaus  20415  2ndc1stc  20543  1stcrest  20545  lly1stc  20588  isref  20601  islocfin  20609  tx1stc  20742  isust  21296  iscfilu  21381  met1stc  21614  iscfil  22313  isgrpo  26005  chne0  27228  pstmfval  28773  dya2iocuni  29178  nobndlem2  30653  nobndlem8  30659  altxpeq1  30811  altxpeq2  30812  elhf2  31013  bj-sngleq  31631  cover2g  32105  indexdom  32125  istotbnd  32165  pmapglb2xN  33408  paddval  33434  elpadd0  33445  diophrex  35689  hbtlem1  36053  hbtlem7  36055
  Copyright terms: Public domain W3C validator