Theorem elrint

Description: Membership in a restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015)

	Ref	Expression
Assertion	elrint	⊢ ( 𝑋 ∈ ( 𝐴 ∩ ∩ 𝐵 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 𝑋 ∈ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		elin	⊢ ( 𝑋 ∈ ( 𝐴 ∩ ∩ 𝐵 ) ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ∈ ∩ 𝐵 ) )
2		elintg	⊢ ( 𝑋 ∈ 𝐴 → ( 𝑋 ∈ ∩ 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 𝑋 ∈ 𝑦 ) )
3	2	pm5.32i	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑋 ∈ ∩ 𝐵 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 𝑋 ∈ 𝑦 ) )
4	1 3	bitri	⊢ ( 𝑋 ∈ ( 𝐴 ∩ ∩ 𝐵 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 𝑋 ∈ 𝑦 ) )