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

Theorem rexeq 3027
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 2585 . 2  |-  F/_ x A
2 nfcv 2585 . 2  |-  F/_ x B
31, 2rexeqf 3023 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 1438   E.wrex 2777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-cleq 2415  df-clel 2418  df-nfc 2573  df-rex 2782
This theorem is referenced by:  rexeqi  3031  rexeqdv  3033  rexeqbi1dv  3035  unieq  4225  exss  4682  qseq1  7419  1sdom  7779  pssnn  7794  indexfi  7886  supeq1  7963  bnd2  8367  dfac2  8563  cflem  8678  cflecard  8685  cfeq0  8688  cfsuc  8689  cfflb  8691  cofsmo  8701  elwina  9113  eltskg  9177  rankcf  9204  elnp  9414  elnpi  9415  genpv  9426  xrsupsslem  11594  xrinfmsslem  11595  xrsupss  11596  xrinfmss  11597  hashge2el2difr  12636  isdrs  16172  isipodrs  16400  neifval  20107  ishaus  20330  2ndc1stc  20458  1stcrest  20460  lly1stc  20503  isref  20516  islocfin  20524  tx1stc  20657  isust  21210  iscfilu  21295  met1stc  21528  iscfil  22227  isgrpo  25916  chne0  27139  pstmfval  28701  dya2iocuni  29107  nobndlem2  30581  nobndlem8  30587  altxpeq1  30739  altxpeq2  30740  elhf2  30941  bj-sngleq  31523  cover2g  31999  indexdom  32019  istotbnd  32059  pmapglb2xN  33300  paddval  33326  elpadd0  33337  diophrex  35581  hbtlem1  35946  hbtlem7  35948
  Copyright terms: Public domain W3C validator