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 ⊢ A ∈ V
Assertion elintrab ⊢ A ∈ ⋂ x ∈ B | φ ↔ ∀ x ∈ B φ → A ∈ x

Proof

Step Hyp Ref Expression
1 elintab.ex ⊢ A ∈ V
2 1 elintab ⊢ A ∈ ⋂ x | x ∈ B ∧ φ ↔ ∀ x x ∈ B ∧ φ → A ∈ x
3 impexp ⊢ x ∈ B ∧ φ → A ∈ x ↔ x ∈ B → φ → A ∈ x
4 3 albii ⊢ ∀ x x ∈ B ∧ φ → A ∈ x ↔ ∀ x x ∈ B → φ → A ∈ x
5 2 4 bitri ⊢ A ∈ ⋂ x | x ∈ B ∧ φ ↔ ∀ x x ∈ B → φ → A ∈ x
6 df-rab ⊢ x ∈ B | φ = x | x ∈ B ∧ φ
7 6 inteqi ⊢ ⋂ x ∈ B | φ = ⋂ x | x ∈ B ∧ φ
8 7 eleq2i ⊢ A ∈ ⋂ x ∈ B | φ ↔ A ∈ ⋂ x | x ∈ B ∧ φ
9 df-ral ⊢ ∀ x ∈ B φ → A ∈ x ↔ ∀ x x ∈ B → φ → A ∈ x
10 5 8 9 3bitr4i ⊢ A ∈ ⋂ x ∈ B | φ ↔ ∀ x ∈ B φ → A ∈ x