Theorem elrabi

Description: Implication for the membership in a restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017) Remove disjoint variable condition on A , x and avoid ax-10 , ax-11 , ax-12 . (Revised by SN, 5-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		dfclel	⊢ ( 𝐴 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑉 ∧ 𝜑 ) } ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑉 ∧ 𝜑 ) } ) )
2		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑉 ∧ 𝜑 ) } ↔ [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝑉 ∧ 𝜑 ) )
3		simpl	⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝜑 ) → 𝑥 ∈ 𝑉 )
4	3	sbimi	⊢ ( [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝑉 ∧ 𝜑 ) → [ 𝑦 / 𝑥 ] 𝑥 ∈ 𝑉 )
5		clelsb3	⊢ ( [ 𝑦 / 𝑥 ] 𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉 )
6	4 5	sylib	⊢ ( [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝑉 ∧ 𝜑 ) → 𝑦 ∈ 𝑉 )
7	2 6	sylbi	⊢ ( 𝑦 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑉 ∧ 𝜑 ) } → 𝑦 ∈ 𝑉 )
8		eleq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉 ) )
9	8	biimpa	⊢ ( ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
10	7 9	sylan2	⊢ ( ( 𝑦 = 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑉 ∧ 𝜑 ) } ) → 𝐴 ∈ 𝑉 )
11	10	exlimiv	⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑉 ∧ 𝜑 ) } ) → 𝐴 ∈ 𝑉 )
12	1 11	sylbi	⊢ ( 𝐴 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑉 ∧ 𝜑 ) } → 𝐴 ∈ 𝑉 )
13		df-rab	⊢ { 𝑥 ∈ 𝑉 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝑉 ∧ 𝜑 ) }
14	12 13	eleq2s	⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝑉 ∣ 𝜑 } → 𝐴 ∈ 𝑉 )