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
|- ( ps -> A e. V )
elab3.2
|- ( x = A -> ( ph <-> ps ) )
Assertion elab3
|- ( A e. { x | ph } <-> ps )

Proof

Step Hyp Ref Expression
1 elab3.1
 |-  ( ps -> A e. V )
2 elab3.2
 |-  ( x = A -> ( ph <-> ps ) )
3 2 elab3g
 |-  ( ( ps -> A e. V ) -> ( A e. { x | ph } <-> ps ) )
4 1 3 ax-mp
 |-  ( A e. { x | ph } <-> ps )