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 ⊢ A ∈ x ∈ V | φ → A ∈ V

Proof

Step Hyp Ref Expression
1 dfclel ⊢ A ∈ x | x ∈ V ∧ φ ↔ ∃ y y = A ∧ y ∈ x | x ∈ V ∧ φ
2 df-clab ⊢ y ∈ x | x ∈ V ∧ φ ↔ y x x ∈ V ∧ φ
3 simpl ⊢ x ∈ V ∧ φ → x ∈ V
4 3 sbimi ⊢ y x x ∈ V ∧ φ → y x x ∈ V
5 clelsb3 ⊢ y x x ∈ V ↔ y ∈ V
6 4 5 sylib ⊢ y x x ∈ V ∧ φ → y ∈ V
7 2 6 sylbi ⊢ y ∈ x | x ∈ V ∧ φ → y ∈ V
8 eleq1 ⊢ y = A → y ∈ V ↔ A ∈ V
9 8 biimpa ⊢ y = A ∧ y ∈ V → A ∈ V
10 7 9 sylan2 ⊢ y = A ∧ y ∈ x | x ∈ V ∧ φ → A ∈ V
11 10 exlimiv ⊢ ∃ y y = A ∧ y ∈ x | x ∈ V ∧ φ → A ∈ V
12 1 11 sylbi ⊢ A ∈ x | x ∈ V ∧ φ → A ∈ V
13 df-rab ⊢ x ∈ V | φ = x | x ∈ V ∧ φ
14 12 13 eleq2s ⊢ A ∈ x ∈ V | φ → A ∈ V