Theorem cbvrexfw

Description: Rule used to change bound variables, using implicit substitution. Version of cbvrexf with a disjoint variable condition, which does not require ax-13 . For a version not dependent on ax-11 and ax-12, see cbvrexvw . (Contributed by FL, 27-Apr-2008) Avoid ax-10 , ax-13 . (Revised by Gino Giotto, 10-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbvrexfw.1	⊢ Ⅎ 𝑥 𝐴
2		cbvrexfw.2	⊢ Ⅎ 𝑦 𝐴
3		cbvrexfw.3	⊢ Ⅎ 𝑦 𝜑
4		cbvrexfw.4	⊢ Ⅎ 𝑥 𝜓
5		cbvrexfw.5	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
6	3	nfn	⊢ Ⅎ 𝑦 ¬ 𝜑
7	4	nfn	⊢ Ⅎ 𝑥 ¬ 𝜓
8	5	notbid	⊢ ( 𝑥 = 𝑦 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
9	1 2 6 7 8	cbvralfw	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝜓 )
10		ralnex	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝜑 )
11		ralnex	⊢ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃ 𝑦 ∈ 𝐴 𝜓 )
12	9 10 11	3bitr3i	⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃ 𝑦 ∈ 𝐴 𝜓 )
13	12	con4bii	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 𝜓 )