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

Metamath Proof Explorer

Theorem elrab3

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

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

Proof

Step Hyp Ref Expression
1 elrab.1 ⊢ x = A → φ ↔ ψ
2 1 elrab ⊢ A ∈ x ∈ B | φ ↔ A ∈ B ∧ ψ
3 2 baib ⊢ A ∈ B → A ∈ x ∈ B | φ ↔ ψ