Metamath Proof Explorer

Theorem elinintrab

Description: Two ways of saying a set is an element of the intersection of a class with the intersection of a class. (Contributed by RP, 14-Aug-2020)

Ref Expression
Assertion elinintrab ⊢ A ∈ V → A ∈ ⋂ w ∈ 𝒫 B | ∃ x w = B ∩ x ∧ φ ↔ ∃ x φ → A ∈ B ∧ ∀ x φ → A ∈ x

Proof

Step Hyp Ref Expression
1 vex ⊢ x ∈ V
2 1 inex2 ⊢ B ∩ x ∈ V
3 inss1 ⊢ B ∩ x ⊆ B
4 2 3 elmapintrab ⊢ A ∈ V → A ∈ ⋂ w ∈ 𝒫 B | ∃ x w = B ∩ x ∧ φ ↔ ∃ x φ → A ∈ B ∧ ∀ x φ → A ∈ B ∩ x
5 elin ⊢ A ∈ B ∩ x ↔ A ∈ B ∧ A ∈ x
6 5 imbi2i ⊢ φ → A ∈ B ∩ x ↔ φ → A ∈ B ∧ A ∈ x
7 jcab ⊢ φ → A ∈ B ∧ A ∈ x ↔ φ → A ∈ B ∧ φ → A ∈ x
8 6 7 bitri ⊢ φ → A ∈ B ∩ x ↔ φ → A ∈ B ∧ φ → A ∈ x
9 8 albii ⊢ ∀ x φ → A ∈ B ∩ x ↔ ∀ x φ → A ∈ B ∧ φ → A ∈ x
10 19.26 ⊢ ∀ x φ → A ∈ B ∧ φ → A ∈ x ↔ ∀ x φ → A ∈ B ∧ ∀ x φ → A ∈ x
11 19.23v ⊢ ∀ x φ → A ∈ B ↔ ∃ x φ → A ∈ B
12 11 anbi1i ⊢ ∀ x φ → A ∈ B ∧ ∀ x φ → A ∈ x ↔ ∃ x φ → A ∈ B ∧ ∀ x φ → A ∈ x
13 10 12 bitri ⊢ ∀ x φ → A ∈ B ∧ φ → A ∈ x ↔ ∃ x φ → A ∈ B ∧ ∀ x φ → A ∈ x
14 9 13 bitri ⊢ ∀ x φ → A ∈ B ∩ x ↔ ∃ x φ → A ∈ B ∧ ∀ x φ → A ∈ x
15 14 anbi2i ⊢ ∃ x φ → A ∈ B ∧ ∀ x φ → A ∈ B ∩ x ↔ ∃ x φ → A ∈ B ∧ ∃ x φ → A ∈ B ∧ ∀ x φ → A ∈ x
16 anabs5 ⊢ ∃ x φ → A ∈ B ∧ ∃ x φ → A ∈ B ∧ ∀ x φ → A ∈ x ↔ ∃ x φ → A ∈ B ∧ ∀ x φ → A ∈ x
17 15 16 bitri ⊢ ∃ x φ → A ∈ B ∧ ∀ x φ → A ∈ B ∩ x ↔ ∃ x φ → A ∈ B ∧ ∀ x φ → A ∈ x
18 4 17 bitrdi ⊢ A ∈ V → A ∈ ⋂ w ∈ 𝒫 B | ∃ x w = B ∩ x ∧ φ ↔ ∃ x φ → A ∈ B ∧ ∀ x φ → A ∈ x