Metamath Proof Explorer

Theorem elmapintrab

Description: Two ways to say a set is an element of the intersection of a class of images. (Contributed by RP, 16-Aug-2020)

Ref Expression
Hypotheses elmapintrab.ex ⊢ C ∈ V
elmapintrab.sub ⊢ C ⊆ B
Assertion elmapintrab ⊢ A ∈ V → A ∈ ⋂ w ∈ 𝒫 B | ∃ x w = C ∧ φ ↔ ∃ x φ → A ∈ B ∧ ∀ x φ → A ∈ C

Proof

Step Hyp Ref Expression
1 elmapintrab.ex ⊢ C ∈ V
2 elmapintrab.sub ⊢ C ⊆ B
3 elintrabg ⊢ A ∈ V → A ∈ ⋂ w ∈ 𝒫 B | ∃ x w = C ∧ φ ↔ ∀ w ∈ 𝒫 B ∃ x w = C ∧ φ → A ∈ w
4 df-ral ⊢ ∀ w ∈ 𝒫 B ∃ x w = C ∧ φ → A ∈ w ↔ ∀ w w ∈ 𝒫 B → ∃ x w = C ∧ φ → A ∈ w
5 3 4 bitrdi ⊢ A ∈ V → A ∈ ⋂ w ∈ 𝒫 B | ∃ x w = C ∧ φ ↔ ∀ w w ∈ 𝒫 B → ∃ x w = C ∧ φ → A ∈ w
6 velpw ⊢ w ∈ 𝒫 B ↔ w ⊆ B
7 19.23v ⊢ ∀ x w = C ∧ φ → A ∈ w ↔ ∃ x w = C ∧ φ → A ∈ w
8 7 bicomi ⊢ ∃ x w = C ∧ φ → A ∈ w ↔ ∀ x w = C ∧ φ → A ∈ w
9 6 8 imbi12i ⊢ w ∈ 𝒫 B → ∃ x w = C ∧ φ → A ∈ w ↔ w ⊆ B → ∀ x w = C ∧ φ → A ∈ w
10 19.21v ⊢ ∀ x w ⊆ B → w = C ∧ φ → A ∈ w ↔ w ⊆ B → ∀ x w = C ∧ φ → A ∈ w
11 bi2.04 ⊢ w ⊆ B → w = C ∧ φ → A ∈ w ↔ w = C ∧ φ → w ⊆ B → A ∈ w
12 impexp ⊢ w = C ∧ φ → w ⊆ B → A ∈ w ↔ w = C → φ → w ⊆ B → A ∈ w
13 11 12 bitri ⊢ w ⊆ B → w = C ∧ φ → A ∈ w ↔ w = C → φ → w ⊆ B → A ∈ w
14 13 albii ⊢ ∀ x w ⊆ B → w = C ∧ φ → A ∈ w ↔ ∀ x w = C → φ → w ⊆ B → A ∈ w
15 9 10 14 3bitr2i ⊢ w ∈ 𝒫 B → ∃ x w = C ∧ φ → A ∈ w ↔ ∀ x w = C → φ → w ⊆ B → A ∈ w
16 15 albii ⊢ ∀ w w ∈ 𝒫 B → ∃ x w = C ∧ φ → A ∈ w ↔ ∀ w ∀ x w = C → φ → w ⊆ B → A ∈ w
17 alcom ⊢ ∀ w ∀ x w = C → φ → w ⊆ B → A ∈ w ↔ ∀ x ∀ w w = C → φ → w ⊆ B → A ∈ w
18 sseq1 ⊢ w = C → w ⊆ B ↔ C ⊆ B
19 eleq2 ⊢ w = C → A ∈ w ↔ A ∈ C
20 2 sseli ⊢ A ∈ C → A ∈ B
21 20 pm4.71ri ⊢ A ∈ C ↔ A ∈ B ∧ A ∈ C
22 19 21 bitrdi ⊢ w = C → A ∈ w ↔ A ∈ B ∧ A ∈ C
23 18 22 imbi12d ⊢ w = C → w ⊆ B → A ∈ w ↔ C ⊆ B → A ∈ B ∧ A ∈ C
24 23 imbi2d ⊢ w = C → φ → w ⊆ B → A ∈ w ↔ φ → C ⊆ B → A ∈ B ∧ A ∈ C
25 1 24 ceqsalv ⊢ ∀ w w = C → φ → w ⊆ B → A ∈ w ↔ φ → C ⊆ B → A ∈ B ∧ A ∈ C
26 bi2.04 ⊢ φ → C ⊆ B → A ∈ B ∧ A ∈ C ↔ C ⊆ B → φ → A ∈ B ∧ A ∈ C
27 pm5.5 ⊢ C ⊆ B → C ⊆ B → φ → A ∈ B ∧ A ∈ C ↔ φ → A ∈ B ∧ A ∈ C
28 2 27 ax-mp ⊢ C ⊆ B → φ → A ∈ B ∧ A ∈ C ↔ φ → A ∈ B ∧ A ∈ C
29 jcab ⊢ φ → A ∈ B ∧ A ∈ C ↔ φ → A ∈ B ∧ φ → A ∈ C
30 28 29 bitri ⊢ C ⊆ B → φ → A ∈ B ∧ A ∈ C ↔ φ → A ∈ B ∧ φ → A ∈ C
31 25 26 30 3bitri ⊢ ∀ w w = C → φ → w ⊆ B → A ∈ w ↔ φ → A ∈ B ∧ φ → A ∈ C
32 31 albii ⊢ ∀ x ∀ w w = C → φ → w ⊆ B → A ∈ w ↔ ∀ x φ → A ∈ B ∧ φ → A ∈ C
33 19.26 ⊢ ∀ x φ → A ∈ B ∧ φ → A ∈ C ↔ ∀ x φ → A ∈ B ∧ ∀ x φ → A ∈ C
34 19.23v ⊢ ∀ x φ → A ∈ B ↔ ∃ x φ → A ∈ B
35 34 anbi1i ⊢ ∀ x φ → A ∈ B ∧ ∀ x φ → A ∈ C ↔ ∃ x φ → A ∈ B ∧ ∀ x φ → A ∈ C
36 32 33 35 3bitri ⊢ ∀ x ∀ w w = C → φ → w ⊆ B → A ∈ w ↔ ∃ x φ → A ∈ B ∧ ∀ x φ → A ∈ C
37 16 17 36 3bitri ⊢ ∀ w w ∈ 𝒫 B → ∃ x w = C ∧ φ → A ∈ w ↔ ∃ x φ → A ∈ B ∧ ∀ x φ → A ∈ C
38 5 37 bitrdi ⊢ A ∈ V → A ∈ ⋂ w ∈ 𝒫 B | ∃ x w = C ∧ φ ↔ ∃ x φ → A ∈ B ∧ ∀ x φ → A ∈ C