Metamath Proof Explorer

Theorem cbvral3v

Description: Change bound variables of triple restricted universal quantification, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvral3vw when possible. (Contributed by NM, 10-May-2005) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cbvral3v.1 ⊢ x = w → φ ↔ χ
2 cbvral3v.2 ⊢ y = v → χ ↔ θ
3 cbvral3v.3 ⊢ z = u → θ ↔ ψ
4 1 2ralbidv ⊢ x = w → ∀ y ∈ B ∀ z ∈ C φ ↔ ∀ y ∈ B ∀ z ∈ C χ
5 4 cbvralv ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C φ ↔ ∀ w ∈ A ∀ y ∈ B ∀ z ∈ C χ
6 2 3 cbvral2v ⊢ ∀ 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 ψ