Theorem cbvrexw

Description: Rule used to change bound variables, using implicit substitution. Version of cbvrex with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 31-Jul-2003) (Revised by Gino Giotto, 10-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbvralw.1	⊢ Ⅎ 𝑦 𝜑
2		cbvralw.2	⊢ Ⅎ 𝑥 𝜓
3		cbvralw.3	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
4		nfcv	⊢ Ⅎ 𝑥 𝐴
5		nfcv	⊢ Ⅎ 𝑦 𝐴
6	4 5 1 2 3	cbvrexfw	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 𝜓 )