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

Theorem rexeq 2916
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 2577 . 2  |-  F/_ x A
2 nfcv 2577 . 2  |-  F/_ x B
31, 2rexeqf 2912 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 1369   E.wrex 2714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rex 2719
This theorem is referenced by:  rexeqi  2920  rexeqdv  2922  rexeqbi1dv  2924  unieq  4097  exss  4553  qseq1  7148  1sdom  7513  pssnn  7529  indexfi  7617  supeq1  7693  bnd2  8098  dfac2  8298  cflem  8413  cflecard  8420  cfeq0  8423  cfsuc  8424  cfflb  8426  cofsmo  8436  elwina  8851  eltskg  8915  rankcf  8942  elnp  9154  elnpi  9155  genpv  9166  xrsupsslem  11267  xrinfmsslem  11268  xrsupss  11269  xrinfmss  11270  isdrs  15102  isipodrs  15329  neifval  18701  ishaus  18924  2ndc1stc  19053  1stcrest  19055  lly1stc  19098  tx1stc  19221  isust  19776  iscfilu  19861  met1stc  20094  iscfil  20774  isgrpo  23681  chne0  24895  pstmfval  26321  dya2iocuni  26696  nobndlem2  27832  nobndlem8  27838  altxpeq1  28002  altxpeq2  28003  elhf2  28211  isref  28548  islocfin  28565  cover2g  28605  indexdom  28625  istotbnd  28665  diophrex  29111  hbtlem1  29476  hbtlem7  29478  bj-sngleq  32457  pmapglb2xN  33413  paddval  33439  elpadd0  33450
  Copyright terms: Public domain W3C validator