Metamath Proof Explorer


Theorem cbvral4vw

Description: Change bound variables of quadruple restricted universal quantification, using implicit substitution. (Contributed by Scott Fenton, 2-Mar-2025)

Ref Expression
Hypotheses cbvral4vw.1 ( 𝑥 = 𝑎 → ( 𝜑𝜒 ) )
cbvral4vw.2 ( 𝑦 = 𝑏 → ( 𝜒𝜃 ) )
cbvral4vw.3 ( 𝑧 = 𝑐 → ( 𝜃𝜏 ) )
cbvral4vw.4 ( 𝑤 = 𝑑 → ( 𝜏𝜓 ) )
Assertion cbvral4vw ( ∀ 𝑥𝐴𝑦𝐵𝑧𝐶𝑤𝐷 𝜑 ↔ ∀ 𝑎𝐴𝑏𝐵𝑐𝐶𝑑𝐷 𝜓 )

Proof

Step Hyp Ref Expression
1 cbvral4vw.1 ( 𝑥 = 𝑎 → ( 𝜑𝜒 ) )
2 cbvral4vw.2 ( 𝑦 = 𝑏 → ( 𝜒𝜃 ) )
3 cbvral4vw.3 ( 𝑧 = 𝑐 → ( 𝜃𝜏 ) )
4 cbvral4vw.4 ( 𝑤 = 𝑑 → ( 𝜏𝜓 ) )
5 1 ralbidv ( 𝑥 = 𝑎 → ( ∀ 𝑤𝐷 𝜑 ↔ ∀ 𝑤𝐷 𝜒 ) )
6 2 ralbidv ( 𝑦 = 𝑏 → ( ∀ 𝑤𝐷 𝜒 ↔ ∀ 𝑤𝐷 𝜃 ) )
7 3 ralbidv ( 𝑧 = 𝑐 → ( ∀ 𝑤𝐷 𝜃 ↔ ∀ 𝑤𝐷 𝜏 ) )
8 5 6 7 cbvral3vw ( ∀ 𝑥𝐴𝑦𝐵𝑧𝐶𝑤𝐷 𝜑 ↔ ∀ 𝑎𝐴𝑏𝐵𝑐𝐶𝑤𝐷 𝜏 )
9 4 cbvralvw ( ∀ 𝑤𝐷 𝜏 ↔ ∀ 𝑑𝐷 𝜓 )
10 9 3ralbii ( ∀ 𝑎𝐴𝑏𝐵𝑐𝐶𝑤𝐷 𝜏 ↔ ∀ 𝑎𝐴𝑏𝐵𝑐𝐶𝑑𝐷 𝜓 )
11 8 10 bitri ( ∀ 𝑥𝐴𝑦𝐵𝑧𝐶𝑤𝐷 𝜑 ↔ ∀ 𝑎𝐴𝑏𝐵𝑐𝐶𝑑𝐷 𝜓 )