Theorem cbvmow

Description: Rule used to change bound variables, using implicit substitution. Version of cbvmo with a disjoint variable condition, which does not require ax-10 , ax-13 . (Contributed by NM, 9-Mar-1995) (Revised by Gino Giotto, 23-May-2024)

	Ref	Expression
Hypotheses	cbvmow.1	⊢ Ⅎ 𝑦 𝜑
	cbvmow.2	⊢ Ⅎ 𝑥 𝜓
	cbvmow.3	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	cbvmow	⊢ ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		cbvmow.1	⊢ Ⅎ 𝑦 𝜑
2		cbvmow.2	⊢ Ⅎ 𝑥 𝜓
3		cbvmow.3	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
4		nfv	⊢ Ⅎ 𝑦 𝑥 = 𝑧
5	1 4	nfim	⊢ Ⅎ 𝑦 ( 𝜑 → 𝑥 = 𝑧 )
6		nfv	⊢ Ⅎ 𝑥 𝑦 = 𝑧
7	2 6	nfim	⊢ Ⅎ 𝑥 ( 𝜓 → 𝑦 = 𝑧 )
8		equequ1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 ↔ 𝑦 = 𝑧 ) )
9	3 8	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 → 𝑥 = 𝑧 ) ↔ ( 𝜓 → 𝑦 = 𝑧 ) ) )
10	5 7 9	cbvalv1	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ↔ ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) )
11	10	exbii	⊢ ( ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ↔ ∃ 𝑧 ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) )
12		df-mo	⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) )
13		df-mo	⊢ ( ∃* 𝑦 𝜓 ↔ ∃ 𝑧 ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) )
14	11 12 13	3bitr4i	⊢ ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 𝜓 )