Metamath Proof Explorer


Theorem elintd

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

Ref Expression
Hypotheses elintd.1 𝑥 𝜑
elintd.2 ( 𝜑𝐴𝑉 )
elintd.3 ( ( 𝜑𝑥𝐵 ) → 𝐴𝑥 )
Assertion elintd ( 𝜑𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 elintd.1 𝑥 𝜑
2 elintd.2 ( 𝜑𝐴𝑉 )
3 elintd.3 ( ( 𝜑𝑥𝐵 ) → 𝐴𝑥 )
4 3 ex ( 𝜑 → ( 𝑥𝐵𝐴𝑥 ) )
5 1 4 ralrimi ( 𝜑 → ∀ 𝑥𝐵 𝐴𝑥 )
6 elintg ( 𝐴𝑉 → ( 𝐴 𝐵 ↔ ∀ 𝑥𝐵 𝐴𝑥 ) )
7 2 6 syl ( 𝜑 → ( 𝐴 𝐵 ↔ ∀ 𝑥𝐵 𝐴𝑥 ) )
8 5 7 mpbird ( 𝜑𝐴 𝐵 )