Metamath Proof Explorer

Theorem cbvral3vw

Description: Change bound variables of triple restricted universal quantification, using implicit substitution. Version of cbvral3v with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 10-May-2005) (Revised by Gino Giotto, 10-Jan-2024)

Ref Expression
Hypotheses cbvral3vw.1 ⊢ x = w → φ ↔ χ
cbvral3vw.2 ⊢ y = v → χ ↔ θ
cbvral3vw.3 ⊢ z = u → θ ↔ ψ
Assertion cbvral3vw ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C φ ↔ ∀ w ∈ A ∀ v ∈ B ∀ u ∈ C ψ

Proof

Step Hyp Ref Expression
1 cbvral3vw.1 ⊢ x = w → φ ↔ χ
2 cbvral3vw.2 ⊢ y = v → χ ↔ θ
3 cbvral3vw.3 ⊢ z = u → θ ↔ ψ
4 1 2ralbidv ⊢ x = w → ∀ y ∈ B ∀ z ∈ C φ ↔ ∀ y ∈ B ∀ z ∈ C χ
5 4 cbvralvw ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C φ ↔ ∀ w ∈ A ∀ y ∈ B ∀ z ∈ C χ
6 2 3 cbvral2vw ⊢ ∀ y ∈ B ∀ z ∈ C χ ↔ ∀ v ∈ B ∀ u ∈ C ψ
7 6 ralbii ⊢ ∀ w ∈ A ∀ y ∈ B ∀ z ∈ C χ ↔ ∀ w ∈ A ∀ v ∈ B ∀ u ∈ C ψ
8 5 7 bitri ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C φ ↔ ∀ w ∈ A ∀ v ∈ B ∀ u ∈ C ψ