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

Theorem cbvexdvaw 2036
Description: Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Version of cbvexdva 2413 with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017.) Avoid ax-13 2375. (Revised by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by Wolf Lammen, 10-Feb-2024.)
Hypothesis
Ref Expression
cbvaldvaw.1 ((𝜑𝑥 = 𝑦) → (𝜓𝜒))
Assertion
Ref Expression
cbvexdvaw (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Distinct variable groups:   𝜓,𝑦   𝜒,𝑥   𝜑,𝑥,𝑦
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑦)

Proof of Theorem cbvexdvaw
StepHypRef Expression
1 cbvaldvaw.1 . . . . 5 ((𝜑𝑥 = 𝑦) → (𝜓𝜒))
21notbid 318 . . . 4 ((𝜑𝑥 = 𝑦) → (¬ 𝜓 ↔ ¬ 𝜒))
32cbvaldvaw 2035 . . 3 (𝜑 → (∀𝑥 ¬ 𝜓 ↔ ∀𝑦 ¬ 𝜒))
4 alnex 1778 . . 3 (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓)
5 alnex 1778 . . 3 (∀𝑦 ¬ 𝜒 ↔ ¬ ∃𝑦𝜒)
63, 4, 53bitr3g 313 . 2 (𝜑 → (¬ ∃𝑥𝜓 ↔ ¬ ∃𝑦𝜒))
76con4bid 317 1 (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wal 1535  wex 1776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777
This theorem is referenced by:  cbvex2vw  2038  isinf  9294  isinfOLD  9295  cbvoprab123vw  36222  cbvoprab13vw  36224  cbveudavw  36234  cbvopab1davw  36247  cbvopab2davw  36248  cbvopabdavw  36249  cbvoprab1davw  36254  cbvoprab2davw  36255  cbvoprab3davw  36256  cbvoprab123davw  36257  cbvoprab12davw  36258  cbvoprab23davw  36259  cbvoprab13davw  36260  bj-gabeqis  36921  grumnud  44282
  Copyright terms: Public domain W3C validator