This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 clelsb1 ⊢ ( [ 𝑦 / 𝑥 ] 𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉 )
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 ⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝑉 ∣ 𝜑 } → 𝐴 ∈ 𝑉 )