Metamath Proof Explorer


Theorem cbvrexdva

Description: Rule used to change the bound variable in a restricted existential quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017) Avoid ax-9 , ax-ext . (Revised by Wolf Lammen, 9-Mar-2025)

Ref Expression
Hypothesis cbvraldva.1 φ x = y ψ χ
Assertion cbvrexdva φ x A ψ y A χ

Proof

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