This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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