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

Theorem cbvexvw 2037
 Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2412 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 320 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
32cbvalvw 2036 . . 3 (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
43notbii 322 . 2 (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
5 df-ex 1774 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
6 df-ex 1774 . 2 (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
74, 5, 63bitr4i 305 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208  ∀wal 1528  ∃wex 1773 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008 This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774 This theorem is referenced by:  cbvex2vw  2041  mojust  2615  mo4  2644  eujust  2650  cbvrexvw  3449  cbvrexdva2  3456  elisset  3504  euind  3713  reuind  3742  cbvopab2v  5135  bm1.3ii  5197  reusv2lem2  5290  relop  5714  dmcoss  5835  fv3  6681  exfo  6864  zfun  7454  suppimacnv  7833  wfrlem1  7946  ac6sfi  8754  brwdom2  9029  aceq1  9535  aceq0  9536  aceq3lem  9538  dfac4  9540  kmlem2  9569  kmlem13  9580  axdc4lem  9869  zfac  9874  zfcndun  10029  zfcndac  10033  sup2  11589  supmul  11605  climmo  14906  summo  15066  prodmo  15282  gsumval3eu  19016  elpt  22172  bnj1185  32053  satf0op  32612  sat1el2xp  32614  frrlem1  33111  bj-bm1.3ii  34344  fdc  35007  cpcoll2d  40580  axc11next  40723  fnchoice  41271  ichexmpl1  43616
 Copyright terms: Public domain W3C validator