Metamath Proof Explorer


Theorem abssdv

Description: Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006) (Proof shortened by SN, 22-Dec-2024)

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

Proof

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