Theorem intmin3

Description: Under subset ordering, the intersection of a class abstraction is less than or equal to any of its members. (Contributed by NM, 3-Jul-2005)

	Ref	Expression
Hypotheses	intmin3.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	intmin3.3	⊢ 𝜓
Assertion	intmin3	⊢ ( 𝐴 ∈ 𝑉 → ∩ { 𝑥 ∣ 𝜑 } ⊆ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		intmin3.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2		intmin3.3	⊢ 𝜓
3	1	elabg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) )
4	2 3	mpbiri	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝑥 ∣ 𝜑 } )
5		intss1	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } → ∩ { 𝑥 ∣ 𝜑 } ⊆ 𝐴 )
6	4 5	syl	⊢ ( 𝐴 ∈ 𝑉 → ∩ { 𝑥 ∣ 𝜑 } ⊆ 𝐴 )