Metamath Proof Explorer


Theorem abssf

Description: Class abstraction in a subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis abssf.1 _ x A
Assertion abssf x | φ A x φ x A

Proof

Step Hyp Ref Expression
1 abssf.1 _ x A
2 1 abid2f x | x A = A
3 2 sseq2i x | φ x | x A x | φ A
4 ss2ab x | φ x | x A x φ x A
5 3 4 bitr3i x | φ A x φ x A