Metamath Proof Explorer

Theorem cbvral2v

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

Ref Expression
Hypotheses cbvral2v.1 ⊢ x = z → φ ↔ χ
cbvral2v.2 ⊢ y = w → χ ↔ ψ
Assertion cbvral2v ⊢ ∀ x ∈ A ∀ y ∈ B φ ↔ ∀ z ∈ A ∀ w ∈ B ψ

Proof

Step Hyp Ref Expression
1 cbvral2v.1 ⊢ x = z → φ ↔ χ
2 cbvral2v.2 ⊢ y = w → χ ↔ ψ
3 1 ralbidv ⊢ x = z → ∀ y ∈ B φ ↔ ∀ y ∈ B χ
4 3 cbvralv ⊢ ∀ x ∈ A ∀ y ∈ B φ ↔ ∀ z ∈ A ∀ y ∈ B χ
5 2 cbvralv ⊢ ∀ y ∈ B χ ↔ ∀ w ∈ B ψ
6 5 ralbii ⊢ ∀ z ∈ A ∀ y ∈ B χ ↔ ∀ z ∈ A ∀ w ∈ B ψ
7 4 6 bitri ⊢ ∀ x ∈ A ∀ y ∈ B φ ↔ ∀ z ∈ A ∀ w ∈ B ψ