Metamath Proof Explorer

Theorem elintima

Description: Element of intersection of images. (Contributed by RP, 13-Apr-2020)

Ref Expression
Assertion elintima ⊢y∈⋂x|∃a∈Ax=aB↔∀a∈A∃b∈Bby∈a

Proof

Step Hyp Ref Expression
1 vex ⊢y∈V
2 1 elint2 ⊢y∈⋂x|∃a∈Ax=aB↔∀z∈x|∃a∈Ax=aBy∈z
3 elequ2 ⊢z=x→y∈z↔y∈x
4 3 ralab2 ⊢∀z∈x|∃a∈Ax=aBy∈z↔∀x∃a∈Ax=aB→y∈x
5 df-rex ⊢∃a∈Ax=aB↔∃aa∈A∧x=aB
6 5 imbi1i ⊢∃a∈Ax=aB→y∈x↔∃aa∈A∧x=aB→y∈x
7 19.23v ⊢∀aa∈A∧x=aB→y∈x↔∃aa∈A∧x=aB→y∈x
8 simpr ⊢a∈A∧x=aB→x=aB
9 8 eleq2d ⊢a∈A∧x=aB→y∈x↔y∈aB
10 9 pm5.74i ⊢a∈A∧x=aB→y∈x↔a∈A∧x=aB→y∈aB
11 1 elima ⊢y∈aB↔∃b∈Bbay
12 df-br ⊢bay↔by∈a
13 12 rexbii ⊢∃b∈Bbay↔∃b∈Bby∈a
14 11 13 bitri ⊢y∈aB↔∃b∈Bby∈a
15 14 imbi2i ⊢a∈A∧x=aB→y∈aB↔a∈A∧x=aB→∃b∈Bby∈a
16 10 15 bitri ⊢a∈A∧x=aB→y∈x↔a∈A∧x=aB→∃b∈Bby∈a
17 16 albii ⊢∀aa∈A∧x=aB→y∈x↔∀aa∈A∧x=aB→∃b∈Bby∈a
18 6 7 17 3bitr2i ⊢∃a∈Ax=aB→y∈x↔∀aa∈A∧x=aB→∃b∈Bby∈a
19 18 albii ⊢∀x∃a∈Ax=aB→y∈x↔∀x∀aa∈A∧x=aB→∃b∈Bby∈a
20 19.23v ⊢∀xa∈A∧x=aB→∃b∈Bby∈a↔∃xa∈A∧x=aB→∃b∈Bby∈a
21 vex ⊢a∈V
22 21 imaex ⊢aB∈V
23 22 isseti ⊢∃xx=aB
24 19.42v ⊢∃xa∈A∧x=aB↔a∈A∧∃xx=aB
25 23 24 mpbiran2 ⊢∃xa∈A∧x=aB↔a∈A
26 25 imbi1i ⊢∃xa∈A∧x=aB→∃b∈Bby∈a↔a∈A→∃b∈Bby∈a
27 20 26 bitri ⊢∀xa∈A∧x=aB→∃b∈Bby∈a↔a∈A→∃b∈Bby∈a
28 27 albii ⊢∀a∀xa∈A∧x=aB→∃b∈Bby∈a↔∀aa∈A→∃b∈Bby∈a
29 alcom ⊢∀x∀aa∈A∧x=aB→∃b∈Bby∈a↔∀a∀xa∈A∧x=aB→∃b∈Bby∈a
30 df-ral ⊢∀a∈A∃b∈Bby∈a↔∀aa∈A→∃b∈Bby∈a
31 28 29 30 3bitr4i ⊢∀x∀aa∈A∧x=aB→∃b∈Bby∈a↔∀a∈A∃b∈Bby∈a
32 19 31 bitri ⊢∀x∃a∈Ax=aB→y∈x↔∀a∈A∃b∈Bby∈a
33 4 32 bitri ⊢∀z∈x|∃a∈Ax=aBy∈z↔∀a∈A∃b∈Bby∈a
34 2 33 bitri ⊢y∈⋂x|∃a∈Ax=aB↔∀a∈A∃b∈Bby∈a