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