Theorem cbvex2v

Description: Rule used to change bound variables, using implicit substitution. Version of cbvex2 with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 14-Sep-2003) (Revised by BJ, 16-Jun-2019)

	Ref	Expression
Hypotheses	cbval2v.1	⊢ Ⅎ 𝑧 𝜑
	cbval2v.2	⊢ Ⅎ 𝑤 𝜑
	cbval2v.3	⊢ Ⅎ 𝑥 𝜓
	cbval2v.4	⊢ Ⅎ 𝑦 𝜓
	cbval2v.5	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion	cbvex2v	⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑧 ∃ 𝑤 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		cbval2v.1	⊢ Ⅎ 𝑧 𝜑
2		cbval2v.2	⊢ Ⅎ 𝑤 𝜑
3		cbval2v.3	⊢ Ⅎ 𝑥 𝜓
4		cbval2v.4	⊢ Ⅎ 𝑦 𝜓
5		cbval2v.5	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝜑 ↔ 𝜓 ) )
6	1	nfn	⊢ Ⅎ 𝑧 ¬ 𝜑
7	2	nfn	⊢ Ⅎ 𝑤 ¬ 𝜑
8	3	nfn	⊢ Ⅎ 𝑥 ¬ 𝜓
9	4	nfn	⊢ Ⅎ 𝑦 ¬ 𝜓
10	5	notbid	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
11	6 7 8 9 10	cbval2v	⊢ ( ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 ↔ ∀ 𝑧 ∀ 𝑤 ¬ 𝜓 )
12		2nexaln	⊢ ( ¬ ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 )
13		2nexaln	⊢ ( ¬ ∃ 𝑧 ∃ 𝑤 𝜓 ↔ ∀ 𝑧 ∀ 𝑤 ¬ 𝜓 )
14	11 12 13	3bitr4i	⊢ ( ¬ ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ¬ ∃ 𝑧 ∃ 𝑤 𝜓 )
15	14	con4bii	⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑧 ∃ 𝑤 𝜓 )