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

Theorem rexeq 3115
Description: Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.)
Assertion
Ref Expression
rexeq (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rexeq
StepHypRef Expression
1 nfcv 2750 . 2 𝑥𝐴
2 nfcv 2750 . 2 𝑥𝐵
31, 2rexeqf 3111 1 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wrex 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rex 2901
This theorem is referenced by:  rexeqi  3119  rexeqdv  3121  rexeqbi1dv  3123  unieq  4374  exss  4852  qseq1  7661  1sdom  8026  pssnn  8041  indexfi  8135  supeq1  8212  bnd2  8617  dfac2  8814  cflem  8929  cflecard  8936  cfeq0  8939  cfsuc  8940  cfflb  8942  cofsmo  8952  elwina  9365  eltskg  9429  rankcf  9456  elnp  9666  elnpi  9667  genpv  9678  xrsupsslem  11968  xrinfmsslem  11969  xrsupss  11970  xrinfmss  11971  hashge2el2difr  13071  isdrs  16706  isipodrs  16933  neifval  20661  ishaus  20884  2ndc1stc  21012  1stcrest  21014  lly1stc  21057  isref  21070  islocfin  21078  tx1stc  21211  isust  21765  iscfilu  21850  met1stc  22084  iscfil  22816  isgrpo  26529  chne0  27571  pstmfval  29101  dya2iocuni  29506  nobndlem2  30926  nobndlem8  30932  altxpeq1  31084  altxpeq2  31085  elhf2  31286  bj-sngleq  31972  cover2g  32503  indexdom  32523  istotbnd  32562  pmapglb2xN  33900  paddval  33926  elpadd0  33937  diophrex  36181  hbtlem1  36536  hbtlem7  36538
  Copyright terms: Public domain W3C validator