Theorem ss2rabi

Description: Inference of restricted abstraction subclass from implication. (Contributed by NM, 14-Oct-1999)

	Ref	Expression
Hypothesis	ss2rabi.1	⊢ ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝜓 ) )
Assertion	ss2rabi	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 }

Proof

Step	Hyp	Ref	Expression
1		ss2rabi.1	⊢ ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝜓 ) )
2		ss2rab	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ↔ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) )
3	2 1	mprgbir	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 }