Theorem rexsb

Description: An equivalent expression for restricted existence, analogous to exsb . (Contributed by Alexander van der Vekens, 1-Jul-2017)

	Ref	Expression
Assertion	rexsb	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑦 𝜑
2		nfa1	⊢ Ⅎ 𝑥 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 )
3		ax12v	⊢ ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
4		sp	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ( 𝑥 = 𝑦 → 𝜑 ) )
5	4	com12	⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → 𝜑 ) )
6	3 5	impbid	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
7	1 2 6	cbvrexw	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )