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

Theorem cbvexdvaw 2037
Description: Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Version of cbvexdva 2414 with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017.) Avoid ax-13 2376. (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 2036 . . 3 (𝜑 → (∀𝑥 ¬ 𝜓 ↔ ∀𝑦 ¬ 𝜒))
4 alnex 1780 . . 3 (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓)
5 alnex 1780 . . 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 1537  wex 1778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779
This theorem is referenced by:  cbvex2vw  2039  isinf  9297  isinfOLD  9298  cbvoprab123vw  36241  cbvoprab13vw  36243  cbveudavw  36253  cbvopab1davw  36266  cbvopab2davw  36267  cbvopabdavw  36268  cbvoprab1davw  36273  cbvoprab2davw  36274  cbvoprab3davw  36275  cbvoprab123davw  36276  cbvoprab12davw  36277  cbvoprab23davw  36278  cbvoprab13davw  36279  bj-gabeqis  36940  grumnud  44310
  Copyright terms: Public domain W3C validator