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 | φ ψ