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

Metamath Proof Explorer

Theorem elrab

Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999) Remove dependency on ax-13 . (Revised by Steven Nguyen, 23-Nov-2022)

Ref Expression
Hypothesis elrab.1 ⊢ x = A → φ ↔ ψ
Assertion elrab ⊢ A ∈ x ∈ B | φ ↔ A ∈ B ∧ ψ

Proof

Step Hyp Ref Expression
1 elrab.1 ⊢ x = A → φ ↔ ψ
2 elex ⊢ A ∈ x ∈ B | φ → A ∈ V
3 elex ⊢ A ∈ B → A ∈ V
4 3 adantr ⊢ A ∈ B ∧ ψ → A ∈ V
5 eleq1 ⊢ x = A → x ∈ B ↔ A ∈ B
6 5 1 anbi12d ⊢ x = A → x ∈ B ∧ φ ↔ A ∈ B ∧ ψ
7 df-rab ⊢ x ∈ B | φ = x | x ∈ B ∧ φ
8 6 7 elab2g ⊢ A ∈ V → A ∈ x ∈ B | φ ↔ A ∈ B ∧ ψ
9 2 4 8 pm5.21nii ⊢ A ∈ x ∈ B | φ ↔ A ∈ B ∧ ψ