Theorem ssriv

Description: Inference based on subclass definition. (Contributed by NM, 21-Jun-1993)

	Ref	Expression
Hypothesis	ssriv.1	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 )
Assertion	ssriv	⊢ 𝐴 ⊆ 𝐵

Proof

Step	Hyp	Ref	Expression
1		ssriv.1	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 )
2		dfss2	⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
3	2 1	mpgbir	⊢ 𝐴 ⊆ 𝐵