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

Metamath Proof Explorer

Theorem elab2

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995)

Ref Expression
Hypotheses elab2.1 ⊢ A ∈ V
elab2.2 ⊢ x = A → φ ↔ ψ
elab2.3 ⊢ B = x | φ
Assertion elab2 ⊢ A ∈ B ↔ ψ

Proof

Step Hyp Ref Expression
1 elab2.1 ⊢ A ∈ V
2 elab2.2 ⊢ x = A → φ ↔ ψ
3 elab2.3 ⊢ B = x | φ
4 2 3 elab2g ⊢ A ∈ V → A ∈ B ↔ ψ
5 1 4 ax-mp ⊢ A ∈ B ↔ ψ