Metamath Proof Explorer

Theorem cbvral2

Description: Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvral2v . (Contributed by Alexander van der Vekens, 2-Jul-2017)

Ref Expression
Hypotheses cbvral2.1 ⊢ Ⅎ z φ
cbvral2.2 ⊢ Ⅎ x χ
cbvral2.3 ⊢ Ⅎ w χ
cbvral2.4 ⊢ Ⅎ y ψ
cbvral2.5 ⊢ x = z → φ ↔ χ
cbvral2.6 ⊢ y = w → χ ↔ ψ
Assertion cbvral2 ⊢ ∀ x ∈ A ∀ y ∈ B φ ↔ ∀ z ∈ A ∀ w ∈ B ψ

Proof

Step Hyp Ref Expression
1 cbvral2.1 ⊢ Ⅎ z φ
2 cbvral2.2 ⊢ Ⅎ x χ
3 cbvral2.3 ⊢ Ⅎ w χ
4 cbvral2.4 ⊢ Ⅎ y ψ
5 cbvral2.5 ⊢ x = z → φ ↔ χ
6 cbvral2.6 ⊢ y = w → χ ↔ ψ
7 nfcv ⊢ Ⅎ _ z B
8 7 1 nfral ⊢ Ⅎ z ∀ y ∈ B φ
9 nfcv ⊢ Ⅎ _ x B
10 9 2 nfral ⊢ Ⅎ x ∀ y ∈ B χ
11 5 ralbidv ⊢ x = z → ∀ y ∈ B φ ↔ ∀ y ∈ B χ
12 8 10 11 cbvralw ⊢ ∀ x ∈ A ∀ y ∈ B φ ↔ ∀ z ∈ A ∀ y ∈ B χ
13 3 4 6 cbvralw ⊢ ∀ y ∈ B χ ↔ ∀ w ∈ B ψ
14 13 ralbii ⊢ ∀ z ∈ A ∀ y ∈ B χ ↔ ∀ z ∈ A ∀ w ∈ B ψ
15 12 14 bitri ⊢ ∀ x ∈ A ∀ y ∈ B φ ↔ ∀ z ∈ A ∀ w ∈ B ψ