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 φ ψ
Assertion elscottab y Scott x | φ ψ

Proof

Step Hyp Ref Expression
1 elscottab.1 x = y φ ψ
2 scottss Scott x | φ x | φ
3 2 sseli y Scott x | φ y x | φ
4 vex y V
5 4 1 elab y x | φ ψ
6 3 5 sylib y Scott x | φ ψ