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 . (Contributed by FL, 27-Apr-2008) (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	9	notbii	⊢ ( ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀ 𝑦 ∈ 𝐴 ¬ 𝜓 )
11		dfrex2	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 )
12		dfrex2	⊢ ( ∃ 𝑦 ∈ 𝐴 𝜓 ↔ ¬ ∀ 𝑦 ∈ 𝐴 ¬ 𝜓 )
13	10 11 12	3bitr4i	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 𝜓 )