Metamath Proof Explorer


Theorem ssabf

Description: Subclass of a class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

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