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

Metamath Proof Explorer

Theorem elrab2

Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 2-Nov-2006)

Ref Expression
Hypotheses elrab2.1 ⊢ x = A → φ ↔ ψ
elrab2.2 ⊢ C = x ∈ B | φ
Assertion elrab2 ⊢ A ∈ C ↔ A ∈ B ∧ ψ

Proof

Step Hyp Ref Expression
1 elrab2.1 ⊢ x = A → φ ↔ ψ
2 elrab2.2 ⊢ C = x ∈ B | φ
3 2 eleq2i ⊢ A ∈ C ↔ A ∈ x ∈ B | φ
4 1 elrab ⊢ A ∈ x ∈ B | φ ↔ A ∈ B ∧ ψ
5 3 4 bitri ⊢ A ∈ C ↔ A ∈ B ∧ ψ