This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvrexw

Description: Rule used to change bound variables, using implicit substitution. Version of cbvrexfw with more disjoint variable conditions. (Contributed by NM, 31-Jul-2003) Avoid ax-13 . (Revised by GG, 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	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 𝜓 )