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	⊢ Ⅎ 𝑧 𝜑
	cbvral2.2	⊢ Ⅎ 𝑥 𝜒
	cbvral2.3	⊢ Ⅎ 𝑤 𝜒
	cbvral2.4	⊢ Ⅎ 𝑦 𝜓
	cbvral2.5	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ 𝜒 ) )
	cbvral2.6	⊢ ( 𝑦 = 𝑤 → ( 𝜒 ↔ 𝜓 ) )
Assertion	cbvral2	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐵 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		cbvral2.1	⊢ Ⅎ 𝑧 𝜑
2		cbvral2.2	⊢ Ⅎ 𝑥 𝜒
3		cbvral2.3	⊢ Ⅎ 𝑤 𝜒
4		cbvral2.4	⊢ Ⅎ 𝑦 𝜓
5		cbvral2.5	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ 𝜒 ) )
6		cbvral2.6	⊢ ( 𝑦 = 𝑤 → ( 𝜒 ↔ 𝜓 ) )
7		nfcv	⊢ Ⅎ 𝑧 𝐵
8	7 1	nfral	⊢ Ⅎ 𝑧 ∀ 𝑦 ∈ 𝐵 𝜑
9		nfcv	⊢ Ⅎ 𝑥 𝐵
10	9 2	nfral	⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝐵 𝜒
11	5	ralbidv	⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 𝜒 ) )
12	8 10 11	cbvralw	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜒 )
13	3 4 6	cbvralw	⊢ ( ∀ 𝑦 ∈ 𝐵 𝜒 ↔ ∀ 𝑤 ∈ 𝐵 𝜓 )
14	13	ralbii	⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜒 ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐵 𝜓 )
15	12 14	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐵 𝜓 )