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

Theorem cbvexvw 2036
Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2406 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 318 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
32cbvalvw 2035 . . 3 (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
43notbii 320 . 2 (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
5 df-ex 1780 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
6 df-ex 1780 . 2 (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
74, 5, 63bitr4i 303 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wal 1538  wex 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780
This theorem is referenced by:  cbvex2vw  2040  mojust  2539  mo4  2566  eujust  2571  cbveuvw  2605  iseqsetvlem  2805  cbvrexvw  3238  cbvrexdva2OLD  3350  euind  3730  reuind  3759  cbvopab1v  5221  cbvopab2v  5223  bm1.3iiOLD  5302  reusv2lem2  5399  relop  5861  dmcoss  5985  fv3  6924  exfo  7125  cbvoprab3v  7525  zfun  7756  suppimacnv  8199  frrlem1  8311  wfrlem1OLD  8348  ac6sfi  9320  brwdom2  9613  ttrclss  9760  ttrclselem2  9766  aceq1  10157  aceq0  10158  aceq3lem  10160  dfac4  10162  kmlem2  10192  kmlem13  10203  axdc4lem  10495  zfac  10500  zfcndun  10655  zfcndac  10659  sup2  12224  supmul  12240  climmo  15593  summo  15753  prodmo  15972  gsumval3eu  19922  elpt  23580  gsumwrd2dccatlem  33069  1arithidomlem1  33563  1arithidom  33565  bnj1185  34807  fineqvac  35111  satf0op  35382  sat1el2xp  35384  cbvrexvw2  36228  cbvoprab1vw  36238  cbvoprab2vw  36239  cbvoprab13vw  36242  bj-bm1.3ii  37065  wl-ax12v2cl  37507  fdc  37752  sn-sup2  42501  cpcoll2d  44278  axc11next  44425  fnchoice  45034  ichexmpl1  47456
  Copyright terms: Public domain W3C validator