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

Theorem rexeq 3169
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 2793 . 2 𝑥𝐴
2 nfcv 2793 . 2 𝑥𝐵
31, 2rexeqf 3165 1 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947
This theorem is referenced by:  rexeqi  3173  rexeqdv  3175  rexeqbi1dv  3177  unieq  4476  exss  4961  qseq1  7839  1sdom  8204  pssnn  8219  indexfi  8315  supeq1  8392  bnd2  8794  dfac2  8991  cflem  9106  cflecard  9113  cfeq0  9116  cfsuc  9117  cfflb  9119  cofsmo  9129  elwina  9546  eltskg  9610  rankcf  9637  elnp  9847  elnpi  9848  genpv  9859  xrsupsslem  12175  xrinfmsslem  12176  xrsupss  12177  xrinfmss  12178  hashge2el2difr  13301  isdrs  16981  isipodrs  17208  neifval  20951  ishaus  21174  2ndc1stc  21302  1stcrest  21304  lly1stc  21347  isref  21360  islocfin  21368  tx1stc  21501  isust  22054  iscfilu  22139  met1stc  22373  iscfil  23109  isgrpo  27479  chne0  28481  pstmfval  30067  dya2iocuni  30473  noetalem3  31990  altxpeq1  32205  altxpeq2  32206  elhf2  32407  bj-sngleq  33080  cover2g  33639  indexdom  33659  istotbnd  33698  pmapglb2xN  35376  paddval  35402  elpadd0  35413  diophrex  37656  hbtlem1  38010  hbtlem7  38012  sprval  42054  sprsymrelfvlem  42065  sprsymrelfv  42069  sprsymrelfo  42072
  Copyright terms: Public domain W3C validator