Theorem cbvrexf

Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvrexfw when possible. (Contributed by FL, 27-Apr-2008) (Revised by Mario Carneiro, 9-Oct-2016) (New usage is discouraged.)

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

Proof

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