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|∃xw=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|∃xw=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|∃xw=B∩x∧φ↔∃xφ→A∈B∧∀xφ→A∈x