Metamath Proof Explorer


Theorem ss2abdv

Description: Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011) (Revised by Steven Nguyen, 28-Jun-2024)

Ref Expression
Hypothesis ss2abdv.1 φ ψ χ
Assertion ss2abdv φ x | ψ x | χ

Proof

Step Hyp Ref Expression
1 ss2abdv.1 φ ψ χ
2 1 sbimdv φ y x ψ y x χ
3 df-clab y x | ψ y x ψ
4 df-clab y x | χ y x χ
5 2 3 4 3imtr4g φ y x | ψ y x | χ
6 5 ssrdv φ x | ψ x | χ