Theorem elintdv

Description: Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Hypotheses	elintdv.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	elintdv.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐴 ∈ 𝑥 )
Assertion	elintdv	⊢ ( 𝜑 → 𝐴 ∈ ∩ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		elintdv.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		elintdv.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐴 ∈ 𝑥 )
3		nfv	⊢ Ⅎ 𝑥 𝜑
4	3 1 2	elintd	⊢ ( 𝜑 → 𝐴 ∈ ∩ 𝐵 )