Metamath Proof Explorer


Theorem ssrabi

Description: Inference of restricted abstraction subclass from implication. (Contributed by Peter Mazsa, 26-Oct-2022)

Ref Expression
Hypothesis ssrabi.1 φψ
Assertion ssrabi xA|φxA|ψ

Proof

Step Hyp Ref Expression
1 ssrabi.1 φψ
2 1 a1i xAφψ
3 2 ss2rabi xA|φxA|ψ