Metamath Proof Explorer


Theorem cbvraldva2

Description: Rule used to change the bound variable in a restricted universal quantifier with implicit substitution which also changes the quantifier domain. Deduction form. (Contributed by David Moews, 1-May-2017)

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

Proof

Step Hyp Ref Expression
1 cbvraldva2.1 ( ( 𝜑𝑥 = 𝑦 ) → ( 𝜓𝜒 ) )
2 cbvraldva2.2 ( ( 𝜑𝑥 = 𝑦 ) → 𝐴 = 𝐵 )
3 simpr ( ( 𝜑𝑥 = 𝑦 ) → 𝑥 = 𝑦 )
4 3 2 eleq12d ( ( 𝜑𝑥 = 𝑦 ) → ( 𝑥𝐴𝑦𝐵 ) )
5 4 1 imbi12d ( ( 𝜑𝑥 = 𝑦 ) → ( ( 𝑥𝐴𝜓 ) ↔ ( 𝑦𝐵𝜒 ) ) )
6 5 expcom ( 𝑥 = 𝑦 → ( 𝜑 → ( ( 𝑥𝐴𝜓 ) ↔ ( 𝑦𝐵𝜒 ) ) ) )
7 6 pm5.74d ( 𝑥 = 𝑦 → ( ( 𝜑 → ( 𝑥𝐴𝜓 ) ) ↔ ( 𝜑 → ( 𝑦𝐵𝜒 ) ) ) )
8 7 cbvalvw ( ∀ 𝑥 ( 𝜑 → ( 𝑥𝐴𝜓 ) ) ↔ ∀ 𝑦 ( 𝜑 → ( 𝑦𝐵𝜒 ) ) )
9 19.21v ( ∀ 𝑥 ( 𝜑 → ( 𝑥𝐴𝜓 ) ) ↔ ( 𝜑 → ∀ 𝑥 ( 𝑥𝐴𝜓 ) ) )
10 19.21v ( ∀ 𝑦 ( 𝜑 → ( 𝑦𝐵𝜒 ) ) ↔ ( 𝜑 → ∀ 𝑦 ( 𝑦𝐵𝜒 ) ) )
11 8 9 10 3bitr3i ( ( 𝜑 → ∀ 𝑥 ( 𝑥𝐴𝜓 ) ) ↔ ( 𝜑 → ∀ 𝑦 ( 𝑦𝐵𝜒 ) ) )
12 11 pm5.74ri ( 𝜑 → ( ∀ 𝑥 ( 𝑥𝐴𝜓 ) ↔ ∀ 𝑦 ( 𝑦𝐵𝜒 ) ) )
13 df-ral ( ∀ 𝑥𝐴 𝜓 ↔ ∀ 𝑥 ( 𝑥𝐴𝜓 ) )
14 df-ral ( ∀ 𝑦𝐵 𝜒 ↔ ∀ 𝑦 ( 𝑦𝐵𝜒 ) )
15 12 13 14 3bitr4g ( 𝜑 → ( ∀ 𝑥𝐴 𝜓 ↔ ∀ 𝑦𝐵 𝜒 ) )