Theorem cbvrex2

Description: Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvrex2v . (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	cbvrex2	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝜓 )

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	nfrex	⊢ Ⅎ 𝑧 ∃ 𝑦 ∈ 𝐵 𝜑
9		nfcv	⊢ Ⅎ 𝑥 𝐵
10	9 2	nfrex	⊢ Ⅎ 𝑥 ∃ 𝑦 ∈ 𝐵 𝜒
11	5	rexbidv	⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 𝜒 ) )
12	8 10 11	cbvrexw	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜒 )
13	3 4 6	cbvrexw	⊢ ( ∃ 𝑦 ∈ 𝐵 𝜒 ↔ ∃ 𝑤 ∈ 𝐵 𝜓 )
14	13	rexbii	⊢ ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜒 ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝜓 )
15	12 14	bitri	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝜓 )