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|∃xw=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|∃xw=C∧φ↔∀w∈𝒫B∃xw=C∧φ→A∈w
4 df-ral ⊢∀w∈𝒫B∃xw=C∧φ→A∈w↔∀ww∈𝒫B→∃xw=C∧φ→A∈w
5 3 4 bitrdi ⊢A∈V→A∈⋂w∈𝒫B|∃xw=C∧φ↔∀ww∈𝒫B→∃xw=C∧φ→A∈w
6 velpw ⊢w∈𝒫B↔w⊆B
7 19.23v ⊢∀xw=C∧φ→A∈w↔∃xw=C∧φ→A∈w
8 7 bicomi ⊢∃xw=C∧φ→A∈w↔∀xw=C∧φ→A∈w
9 6 8 imbi12i ⊢w∈𝒫B→∃xw=C∧φ→A∈w↔w⊆B→∀xw=C∧φ→A∈w
10 19.21v ⊢∀xw⊆B→w=C∧φ→A∈w↔w⊆B→∀xw=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 ⊢∀xw⊆B→w=C∧φ→A∈w↔∀xw=C→φ→w⊆B→A∈w
15 9 10 14 3bitr2i ⊢w∈𝒫B→∃xw=C∧φ→A∈w↔∀xw=C→φ→w⊆B→A∈w
16 15 albii ⊢∀ww∈𝒫B→∃xw=C∧φ→A∈w↔∀w∀xw=C→φ→w⊆B→A∈w
17 alcom ⊢∀w∀xw=C→φ→w⊆B→A∈w↔∀x∀ww=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 ⊢∀ww=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 ⊢∀ww=C→φ→w⊆B→A∈w↔φ→A∈B∧φ→A∈C
32 31 albii ⊢∀x∀ww=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∀ww=C→φ→w⊆B→A∈w↔∃xφ→A∈B∧∀xφ→A∈C
37 16 17 36 3bitri ⊢∀ww∈𝒫B→∃xw=C∧φ→A∈w↔∃xφ→A∈B∧∀xφ→A∈C
38 5 37 bitrdi ⊢A∈V→A∈⋂w∈𝒫B|∃xw=C∧φ↔∃xφ→A∈B∧∀xφ→A∈C