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

Theorem cbvexvw 2035
Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2410 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 319 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
32cbvalvw 2034 . . 3 (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
43notbii 321 . 2 (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
5 df-ex 1772 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
6 df-ex 1772 . 2 (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
74, 5, 63bitr4i 304 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wal 1526  wex 1771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772
This theorem is referenced by:  cbvex2vw  2039  mojust  2614  mo4  2643  eujust  2649  cbvrexvw  3448  cbvrexdva2  3455  elisset  3503  euind  3712  reuind  3741  cbvopab2v  5135  bm1.3ii  5197  reusv2lem2  5290  relop  5714  dmcoss  5835  fv3  6681  exfo  6863  zfun  7451  suppimacnv  7830  wfrlem1  7943  ac6sfi  8750  brwdom2  9025  aceq1  9531  aceq0  9532  aceq3lem  9534  dfac4  9536  kmlem2  9565  kmlem13  9576  axdc4lem  9865  zfac  9870  zfcndun  10025  zfcndac  10029  sup2  11585  supmul  11601  climmo  14902  summo  15062  prodmo  15278  gsumval3eu  18953  elpt  22108  bnj1185  31964  satf0op  32521  sat1el2xp  32523  frrlem1  33020  bj-bm1.3ii  34251  fdc  34901  cpcoll2d  40472  axc11next  40615  fnchoice  41163  ichexmpl1  43508
  Copyright terms: Public domain W3C validator