Metamath Proof Explorer


Theorem ssabdv

Description: Deduction of abstraction subclass from implication. (Contributed by SN, 22-Dec-2024)

Ref Expression
Hypothesis ssabdv.1 φ x A ψ
Assertion ssabdv φ A x | ψ

Proof

Step Hyp Ref Expression
1 ssabdv.1 φ x A ψ
2 abid1 A = x | x A
3 1 ss2abdv φ x | x A x | ψ
4 2 3 eqsstrid φ A x | ψ