Theorem elrabi

Description: Implication for the membership in a restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017)

	Ref	Expression
Assertion	elrabi	⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝑉 ∣ 𝜑 } → 𝐴 ∈ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		clelab	⊢ ( 𝐴 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑉 ∧ 𝜑 ) } ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝜑 ) ) )
2		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉 ) )
3	2	anbi1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝑉 ∧ 𝜑 ) ↔ ( 𝐴 ∈ 𝑉 ∧ 𝜑 ) ) )
4	3	simprbda	⊢ ( ( 𝑥 = 𝐴 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝜑 ) ) → 𝐴 ∈ 𝑉 )
5	4	exlimiv	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝜑 ) ) → 𝐴 ∈ 𝑉 )
6	1 5	sylbi	⊢ ( 𝐴 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑉 ∧ 𝜑 ) } → 𝐴 ∈ 𝑉 )
7		df-rab	⊢ { 𝑥 ∈ 𝑉 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝑉 ∧ 𝜑 ) }
8	6 7	eleq2s	⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝑉 ∣ 𝜑 } → 𝐴 ∈ 𝑉 )