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

Metamath Proof Explorer

Theorem elab3

Description: Membership in a class abstraction using implicit substitution. (Contributed by NM, 10-Nov-2000) (Revised by AV, 16-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 elab3.1 ⊢ ψ → A ∈ V
2 elab3.2 ⊢ x = A → φ ↔ ψ
3 2 elab3g ⊢ ψ → A ∈ V → A ∈ x | φ ↔ ψ
4 1 3 ax-mp ⊢ A ∈ x | φ ↔ ψ