Metamath Proof Explorer


Theorem ss2ab1

Description: Class abstractions in a subclass relationship, closed form. One direction of ss2ab using fewer axioms. (Contributed by SN, 22-Dec-2024)

Ref Expression
Assertion ss2ab1 x φ ψ x | φ x | ψ

Proof

Step Hyp Ref Expression
1 spsbim x φ ψ t x φ t x ψ
2 df-clab t x | φ t x φ
3 df-clab t x | ψ t x ψ
4 1 2 3 3imtr4g x φ ψ t x | φ t x | ψ
5 4 ssrdv x φ ψ x | φ x | ψ