Metamath Proof Explorer

Theorem cbvexdvaw

Description: Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Version of cbvexdva with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017) (Revised by Gino Giotto, 10-Jan-2024) Reduce axiom usage. (Revised by Wolf Lammen, 10-Feb-2024)

Ref Expression
Hypothesis cbvaldvaw.1 φ x = y ψ χ
Assertion cbvexdvaw φ x ψ y χ


Step Hyp Ref Expression
1 cbvaldvaw.1 φ x = y ψ χ
2 1 notbid φ x = y ¬ ψ ¬ χ
3 2 cbvaldvaw φ x ¬ ψ y ¬ χ
4 alnex x ¬ ψ ¬ x ψ
5 alnex y ¬ χ ¬ y χ
6 3 4 5 3bitr3g φ ¬ x ψ ¬ y χ
7 6 con4bid φ x ψ y χ