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

Theorem cbvexvw 2139
Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2413 for a version with fewer disjoint variable 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 310 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
32cbvalvw 2138 . . 3 (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
43notbii 312 . 2 (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
5 df-ex 1876 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
6 df-ex 1876 . 2 (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
74, 5, 63bitr4i 295 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wal 1651  wex 1875
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107
This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876
This theorem is referenced by:  mojust  2590  eujust  2611  euind  3589  reuind  3609  cbvopab2v  4920  bm1.3ii  4978  reusv2lem2  5069  relop  5476  dmcoss  5589  fv3  6429  exfo  6603  zfun  7184  suppimacnv  7543  wfrlem1  7652  ac6sfi  8446  brwdom2  8720  aceq1  9226  aceq0  9227  aceq3lem  9229  dfac4  9231  kmlem2  9261  kmlem13  9272  axdc4lem  9565  zfac  9570  zfcndun  9725  zfcndac  9729  sup2  11271  supmul  11287  climmo  14629  summo  14789  prodmo  15003  gsumval3eu  18620  elpt  21704  bnj1185  31381  frrlem1  32293  bj-denotesv  33349  bj-bm1.3ii  33516  fdc  34028  axc11next  39388  fnchoice  39948
  Copyright terms: Public domain W3C validator