Metamath Proof Explorer


Theorem cbvrexdva2

Description: Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. Deduction form. (Contributed by David Moews, 1-May-2017) (Proof shortened by Wolf Lammen, 8-Jan-2025)

Ref Expression
Hypotheses cbvraldva2.1 ( ( 𝜑𝑥 = 𝑦 ) → ( 𝜓𝜒 ) )
cbvraldva2.2 ( ( 𝜑𝑥 = 𝑦 ) → 𝐴 = 𝐵 )
Assertion cbvrexdva2 ( 𝜑 → ( ∃ 𝑥𝐴 𝜓 ↔ ∃ 𝑦𝐵 𝜒 ) )

Proof

Step Hyp Ref Expression
1 cbvraldva2.1 ( ( 𝜑𝑥 = 𝑦 ) → ( 𝜓𝜒 ) )
2 cbvraldva2.2 ( ( 𝜑𝑥 = 𝑦 ) → 𝐴 = 𝐵 )
3 1 notbid ( ( 𝜑𝑥 = 𝑦 ) → ( ¬ 𝜓 ↔ ¬ 𝜒 ) )
4 3 2 cbvraldva2 ( 𝜑 → ( ∀ 𝑥𝐴 ¬ 𝜓 ↔ ∀ 𝑦𝐵 ¬ 𝜒 ) )
5 ralnex ( ∀ 𝑥𝐴 ¬ 𝜓 ↔ ¬ ∃ 𝑥𝐴 𝜓 )
6 ralnex ( ∀ 𝑦𝐵 ¬ 𝜒 ↔ ¬ ∃ 𝑦𝐵 𝜒 )
7 4 5 6 3bitr3g ( 𝜑 → ( ¬ ∃ 𝑥𝐴 𝜓 ↔ ¬ ∃ 𝑦𝐵 𝜒 ) )
8 7 con4bid ( 𝜑 → ( ∃ 𝑥𝐴 𝜓 ↔ ∃ 𝑦𝐵 𝜒 ) )