Theorem cbvex1v

Description: Rule used to change bound variables, using implicit substitution. (Contributed by BTernaryTau, 31-Jul-2025)

	Ref	Expression
Hypotheses	cbvex1v.1	⊢ Ⅎ 𝑥 𝜑
	cbvex1v.2	⊢ Ⅎ 𝑦 𝜑
	cbvex1v.3	⊢ ( 𝜑 → Ⅎ 𝑦 𝜓 )
	cbvex1v.4	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
	cbvex1v.5	⊢ ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓 → 𝜒 ) ) )
Assertion	cbvex1v	⊢ ( 𝜑 → ( ∃ 𝑥 𝜓 → ∃ 𝑦 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		cbvex1v.1	⊢ Ⅎ 𝑥 𝜑
2		cbvex1v.2	⊢ Ⅎ 𝑦 𝜑
3		cbvex1v.3	⊢ ( 𝜑 → Ⅎ 𝑦 𝜓 )
4		cbvex1v.4	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
5		cbvex1v.5	⊢ ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓 → 𝜒 ) ) )
6	4	nfnd	⊢ ( 𝜑 → Ⅎ 𝑥 ¬ 𝜒 )
7	3	nfnd	⊢ ( 𝜑 → Ⅎ 𝑦 ¬ 𝜓 )
8		equcomi	⊢ ( 𝑦 = 𝑥 → 𝑥 = 𝑦 )
9		con3	⊢ ( ( 𝜓 → 𝜒 ) → ( ¬ 𝜒 → ¬ 𝜓 ) )
10	8 5 9	syl56	⊢ ( 𝜑 → ( 𝑦 = 𝑥 → ( ¬ 𝜒 → ¬ 𝜓 ) ) )
11	2 1 6 7 10	cbv1v	⊢ ( 𝜑 → ( ∀ 𝑦 ¬ 𝜒 → ∀ 𝑥 ¬ 𝜓 ) )
12	11	con3d	⊢ ( 𝜑 → ( ¬ ∀ 𝑥 ¬ 𝜓 → ¬ ∀ 𝑦 ¬ 𝜒 ) )
13		df-ex	⊢ ( ∃ 𝑥 𝜓 ↔ ¬ ∀ 𝑥 ¬ 𝜓 )
14		df-ex	⊢ ( ∃ 𝑦 𝜒 ↔ ¬ ∀ 𝑦 ¬ 𝜒 )
15	12 13 14	3imtr4g	⊢ ( 𝜑 → ( ∃ 𝑥 𝜓 → ∃ 𝑦 𝜒 ) )