Metamath Proof Explorer


Theorem elscottab

Description: An element of the output of the Scott operation applied to a class abstraction satisfies the class abstraction's predicate. (Contributed by Rohan Ridenour, 14-Aug-2023)

Ref Expression
Hypothesis elscottab.1
|- ( x = y -> ( ph <-> ps ) )
Assertion elscottab
|- ( y e. Scott { x | ph } -> ps )

Proof

Step Hyp Ref Expression
1 elscottab.1
 |-  ( x = y -> ( ph <-> ps ) )
2 scottss
 |-  Scott { x | ph } C_ { x | ph }
3 2 sseli
 |-  ( y e. Scott { x | ph } -> y e. { x | ph } )
4 vex
 |-  y e. _V
5 4 1 elab
 |-  ( y e. { x | ph } <-> ps )
6 3 5 sylib
 |-  ( y e. Scott { x | ph } -> ps )