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

Theorem cbvexvw 2041
Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2402 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 2040 . . 3 (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
43notbii 320 . 2 (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
5 df-ex 1783 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
6 df-ex 1783 . 2 (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
74, 5, 63bitr4i 303 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wal 1537  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783
This theorem is referenced by:  cbvex2vw  2045  mojust  2540  mo4  2567  eujust  2572  cbveuvw  2607  clelab  2884  cbvrexvw  3385  cbvrexdva2  3394  euind  3660  reuind  3689  cbvopab1v  5154  cbvopab2v  5156  bm1.3ii  5227  reusv2lem2  5323  relop  5762  dmcoss  5883  fv3  6801  exfo  6990  zfun  7598  suppimacnv  7999  frrlem1  8111  wfrlem1OLD  8148  ac6sfi  9067  brwdom2  9341  ttrclss  9487  ttrclselem2  9493  aceq1  9882  aceq0  9883  aceq3lem  9885  dfac4  9887  kmlem2  9916  kmlem13  9927  axdc4lem  10220  zfac  10225  zfcndun  10380  zfcndac  10384  sup2  11940  supmul  11956  climmo  15275  summo  15438  prodmo  15655  gsumval3eu  19514  elpt  22732  bnj1185  32782  fineqvac  33075  satf0op  33348  sat1el2xp  33350  bj-bm1.3ii  35244  fdc  35912  sn-sup2  40446  cpcoll2d  41884  axc11next  42031  fnchoice  42579  ichexmpl1  44932
  Copyright terms: Public domain W3C validator