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 2400 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 1540  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 398  df-ex 1783
This theorem is referenced by:  cbvex2vw  2045  mojust  2538  mo4  2565  eujust  2570  cbveuvw  2605  clelab  2884  cbvrexvw  3229  cbvrexdva2OLD  3328  euind  3687  reuind  3716  cbvopab1v  5189  cbvopab2v  5191  bm1.3ii  5264  reusv2lem2  5359  relop  5811  dmcoss  5931  fv3  6865  exfo  7060  zfun  7678  suppimacnv  8110  frrlem1  8222  wfrlem1OLD  8259  ac6sfi  9238  brwdom2  9516  ttrclss  9663  ttrclselem2  9669  aceq1  10060  aceq0  10061  aceq3lem  10063  dfac4  10065  kmlem2  10094  kmlem13  10105  axdc4lem  10398  zfac  10403  zfcndun  10558  zfcndac  10562  sup2  12118  supmul  12134  climmo  15446  summo  15609  prodmo  15826  gsumval3eu  19688  elpt  22939  bnj1185  33445  fineqvac  33738  satf0op  34011  sat1el2xp  34013  bj-bm1.3ii  35564  fdc  36233  sn-sup2  40967  cpcoll2d  42613  axc11next  42760  fnchoice  43308  ichexmpl1  45735
  Copyright terms: Public domain W3C validator