Theorem ssmin

Description: Subclass of the minimum value of class of supersets. (Contributed by NM, 10-Aug-2006)

	Ref	Expression
Assertion	ssmin	⊢ 𝐴 ⊆ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ 𝜑 ) }

Proof

Step	Hyp	Ref	Expression
1		ssintab	⊢ ( 𝐴 ⊆ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ 𝜑 ) } ↔ ∀ 𝑥 ( ( 𝐴 ⊆ 𝑥 ∧ 𝜑 ) → 𝐴 ⊆ 𝑥 ) )
2		simpl	⊢ ( ( 𝐴 ⊆ 𝑥 ∧ 𝜑 ) → 𝐴 ⊆ 𝑥 )
3	1 2	mpgbir	⊢ 𝐴 ⊆ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ 𝜑 ) }