Theorem elrint2

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

	Ref	Expression
Assertion	elrint2	⊢ ( 𝑋 ∈ 𝐴 → ( 𝑋 ∈ ( 𝐴 ∩ ∩ 𝐵 ) ↔ ∀ 𝑦 ∈ 𝐵 𝑋 ∈ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		elrint	⊢ ( 𝑋 ∈ ( 𝐴 ∩ ∩ 𝐵 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 𝑋 ∈ 𝑦 ) )
2	1	baib	⊢ ( 𝑋 ∈ 𝐴 → ( 𝑋 ∈ ( 𝐴 ∩ ∩ 𝐵 ) ↔ ∀ 𝑦 ∈ 𝐵 𝑋 ∈ 𝑦 ) )