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

Metamath Proof Explorer

Theorem elintrab

Description: Membership in the intersection of a class abstraction. (Contributed by NM, 17-Oct-1999)

Ref Expression
Hypothesis elintab.ex ⊢ 𝐴 ∈ V
Assertion elintrab ( 𝐴 ∈ ∩ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ ∀ 𝑥 ∈ 𝐵 ( 𝜑 → 𝐴 ∈ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 elintab.ex ⊢ 𝐴 ∈ V
2 1 elintab ⊢ ( 𝐴 ∈ ∩ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } ↔ ∀ 𝑥 ( ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) → 𝐴 ∈ 𝑥 ) )
3 impexp ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) → 𝐴 ∈ 𝑥 ) ↔ ( 𝑥 ∈ 𝐵 → ( 𝜑 → 𝐴 ∈ 𝑥 ) ) )
4 3 albii ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) → 𝐴 ∈ 𝑥 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( 𝜑 → 𝐴 ∈ 𝑥 ) ) )
5 2 4 bitri ⊢ ( 𝐴 ∈ ∩ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( 𝜑 → 𝐴 ∈ 𝑥 ) ) )
6 df-rab ⊢ { 𝑥 ∈ 𝐵 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) }
7 6 inteqi ⊢ ∩ { 𝑥 ∈ 𝐵 ∣ 𝜑 } = ∩ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) }
8 7 eleq2i ⊢ ( 𝐴 ∈ ∩ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ 𝐴 ∈ ∩ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } )
9 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝜑 → 𝐴 ∈ 𝑥 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( 𝜑 → 𝐴 ∈ 𝑥 ) ) )
10 5 8 9 3bitr4i ⊢ ( 𝐴 ∈ ∩ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ ∀ 𝑥 ∈ 𝐵 ( 𝜑 → 𝐴 ∈ 𝑥 ) )