Theorem cbvrmow

Description: Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Version of cbvrmo with a disjoint variable condition, which does not require ax-10 , ax-13 . (Contributed by NM, 16-Jun-2017) (Revised by Gino Giotto, 23-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbvrmow.1	⊢ Ⅎ 𝑦 𝜑
2		cbvrmow.2	⊢ Ⅎ 𝑥 𝜓
3		cbvrmow.3	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
4		nfv	⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
5	4 1	nfan	⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 )
6		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
7	6 2	nfan	⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝜓 )
8		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
9	8 3	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) )
10	5 7 9	cbvmow	⊢ ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃* 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) )
11		df-rmo	⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
12		df-rmo	⊢ ( ∃* 𝑦 ∈ 𝐴 𝜓 ↔ ∃* 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) )
13	10 11 12	3bitr4i	⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑦 ∈ 𝐴 𝜓 )