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

Theorem cbvexvw 2049
Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2401 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 321 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
32cbvalvw 2048 . . 3 (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
43notbii 323 . 2 (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
5 df-ex 1787 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
6 df-ex 1787 . 2 (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
74, 5, 63bitr4i 306 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wal 1540  wex 1786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787
This theorem is referenced by:  cbvex2vw  2053  mojust  2539  mo4  2566  eujust  2572  cbveuvw  2607  clelab  2875  cbvrexvw  3350  cbvrexdva2  3359  euind  3623  reuind  3652  cbvopab2v  5108  bm1.3ii  5170  reusv2lem2  5266  relop  5693  dmcoss  5814  fv3  6694  exfo  6883  zfun  7482  suppimacnv  7871  wfrlem1  7985  ac6sfi  8838  brwdom2  9112  aceq1  9619  aceq0  9620  aceq3lem  9622  dfac4  9624  kmlem2  9653  kmlem13  9664  axdc4lem  9957  zfac  9962  zfcndun  10117  zfcndac  10121  sup2  11676  supmul  11692  climmo  15006  summo  15169  prodmo  15384  gsumval3eu  19145  elpt  22325  bnj1185  32346  fineqvac  32639  satf0op  32912  sat1el2xp  32914  frrlem1  33445  bj-bm1.3ii  34880  fdc  35548  sn-sup2  40038  cpcoll2d  41441  axc11next  41584  fnchoice  42132  ichexmpl1  44484
  Copyright terms: Public domain W3C validator