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

Theorem cbvexvw 2129
Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2438 for a version with fewer DV conditions but requiring more axioms. (Contributed by NM, 19-Apr-2017.)
Hypothesis
Ref Expression
cbvalvw.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvexvw (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Distinct variable groups:   𝑥,𝑦   𝜓,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvexvw
StepHypRef Expression
1 cbvalvw.1 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
21notbid 308 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
32cbvalvw 2128 . . 3 (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
43notbii 310 . 2 (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
5 df-ex 1856 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
6 df-ex 1856 . 2 (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
74, 5, 63bitr4i 293 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wal 1632  wex 1855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096
This theorem depends on definitions:  df-bi 198  df-an 384  df-ex 1856
This theorem is referenced by:  eujust  2623  euind  3551  reuind  3569  cbvopab2v  4874  bm1.3ii  4931  reusv2lem2  5013  relop  5423  dmcoss  5535  fv3  6364  exfo  6537  zfun  7118  suppimacnv  7478  wfrlem1  7587  ac6sfi  8381  brwdom2  8655  aceq1  9161  aceq0  9162  aceq3lem  9164  dfac4  9166  kmlem2  9196  kmlem13  9207  axdc4lem  9500  zfac  9505  zfcndun  9660  zfcndac  9664  sup2  11202  supmul  11218  climmo  14518  summo  14678  prodmo  14895  gsumval3eu  18532  elpt  21616  bnj1185  31219  frrlem1  32134  bj-denotesv  33204  bj-bm1.3ii  33372  fdc  33889  axc11next  39146  fnchoice  39722
  Copyright terms: Public domain W3C validator