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 { 𝑥𝐴𝜑 } ⊆ { 𝑥𝐴𝜓 }

Proof

Step Hyp Ref Expression
1 ssrabi.1 ( 𝜑𝜓 )
2 1 a1i ( 𝑥𝐴 → ( 𝜑𝜓 ) )
3 2 ss2rabi { 𝑥𝐴𝜑 } ⊆ { 𝑥𝐴𝜓 }