Metamath Proof Explorer

Theorem elintfv

Description: Membership in an intersection of function values. (Contributed by Scott Fenton, 9-Dec-2021)

Ref Expression
Hypothesis elintfv.1 ⊢X∈V
Assertion elintfv ⊢FFnA∧B⊆A→X∈⋂FB↔∀y∈BX∈F⁡y

Proof

Step Hyp Ref Expression
1 elintfv.1 ⊢X∈V
2 1 elint ⊢X∈⋂FB↔∀zz∈FB→X∈z
3 fvelimab ⊢FFnA∧B⊆A→z∈FB↔∃y∈BF⁡y=z
4 3 imbi1d ⊢FFnA∧B⊆A→z∈FB→X∈z↔∃y∈BF⁡y=z→X∈z
5 r19.23v ⊢∀y∈BF⁡y=z→X∈z↔∃y∈BF⁡y=z→X∈z
6 4 5 bitr4di ⊢FFnA∧B⊆A→z∈FB→X∈z↔∀y∈BF⁡y=z→X∈z
7 6 albidv ⊢FFnA∧B⊆A→∀zz∈FB→X∈z↔∀z∀y∈BF⁡y=z→X∈z
8 ralcom4 ⊢∀y∈B∀zF⁡y=z→X∈z↔∀z∀y∈BF⁡y=z→X∈z
9 eqcom ⊢F⁡y=z↔z=F⁡y
10 9 imbi1i ⊢F⁡y=z→X∈z↔z=F⁡y→X∈z
11 10 albii ⊢∀zF⁡y=z→X∈z↔∀zz=F⁡y→X∈z
12 fvex ⊢F⁡y∈V
13 eleq2 ⊢z=F⁡y→X∈z↔X∈F⁡y
14 12 13 ceqsalv ⊢∀zz=F⁡y→X∈z↔X∈F⁡y
15 11 14 bitri ⊢∀zF⁡y=z→X∈z↔X∈F⁡y
16 15 ralbii ⊢∀y∈B∀zF⁡y=z→X∈z↔∀y∈BX∈F⁡y
17 8 16 bitr3i ⊢∀z∀y∈BF⁡y=z→X∈z↔∀y∈BX∈F⁡y
18 7 17 bitrdi ⊢FFnA∧B⊆A→∀zz∈FB→X∈z↔∀y∈BX∈F⁡y
19 2 18 bitrid ⊢FFnA∧B⊆A→X∈⋂FB↔∀y∈BX∈F⁡y