This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elint2

Description: Membership in class intersection. (Contributed by NM, 14-Oct-1999)

Ref Expression
Hypothesis elint2.1 ⊢ 𝐴 ∈ V
Assertion elint2 ( 𝐴 ∈ ∩ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 )

Proof

Step Hyp Ref Expression
1 elint2.1 ⊢ 𝐴 ∈ V
2 1 elint ⊢ ( 𝐴 ∈ ∩ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥 ) )
3 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥 ) )
4 2 3 bitr4i ⊢ ( 𝐴 ∈ ∩ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 )