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

Metamath Proof Explorer

Theorem cbvrexv2

Description: Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by David Moews, 1-May-2017) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cbvralv2.1	⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) )
	cbvralv2.2	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
Assertion	cbvrexv2	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑦 ∈ 𝐵 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		cbvralv2.1	⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) )
2		cbvralv2.2	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
3		nfcv	⊢ Ⅎ 𝑦 𝐴
4		nfcv	⊢ Ⅎ 𝑥 𝐵
5		nfv	⊢ Ⅎ 𝑦 𝜓
6		nfv	⊢ Ⅎ 𝑥 𝜒
7	3 4 5 6 2 1	cbvrexcsf	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑦 ∈ 𝐵 𝜒 )