# 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}\in \mathrm{V}$
Assertion elintfv ${⊢}\left({F}Fn{A}\wedge {B}\subseteq {A}\right)\to \left({X}\in \bigcap {F}\left[{B}\right]↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{X}\in {F}\left({y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 elintfv.1 ${⊢}{X}\in \mathrm{V}$
2 1 elint ${⊢}{X}\in \bigcap {F}\left[{B}\right]↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {F}\left[{B}\right]\to {X}\in {z}\right)$
3 fvelimab ${⊢}\left({F}Fn{A}\wedge {B}\subseteq {A}\right)\to \left({z}\in {F}\left[{B}\right]↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)={z}\right)$
4 3 imbi1d ${⊢}\left({F}Fn{A}\wedge {B}\subseteq {A}\right)\to \left(\left({z}\in {F}\left[{B}\right]\to {X}\in {z}\right)↔\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)={z}\to {X}\in {z}\right)\right)$
5 r19.23v ${⊢}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({y}\right)={z}\to {X}\in {z}\right)↔\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)={z}\to {X}\in {z}\right)$
6 4 5 syl6bbr ${⊢}\left({F}Fn{A}\wedge {B}\subseteq {A}\right)\to \left(\left({z}\in {F}\left[{B}\right]\to {X}\in {z}\right)↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({y}\right)={z}\to {X}\in {z}\right)\right)$
7 6 albidv ${⊢}\left({F}Fn{A}\wedge {B}\subseteq {A}\right)\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {F}\left[{B}\right]\to {X}\in {z}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({y}\right)={z}\to {X}\in {z}\right)\right)$
8 ralcom4 ${⊢}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({F}\left({y}\right)={z}\to {X}\in {z}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({y}\right)={z}\to {X}\in {z}\right)$
9 eqcom ${⊢}{F}\left({y}\right)={z}↔{z}={F}\left({y}\right)$
10 9 imbi1i ${⊢}\left({F}\left({y}\right)={z}\to {X}\in {z}\right)↔\left({z}={F}\left({y}\right)\to {X}\in {z}\right)$
11 10 albii ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({F}\left({y}\right)={z}\to {X}\in {z}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={F}\left({y}\right)\to {X}\in {z}\right)$
12 fvex ${⊢}{F}\left({y}\right)\in \mathrm{V}$
13 eleq2 ${⊢}{z}={F}\left({y}\right)\to \left({X}\in {z}↔{X}\in {F}\left({y}\right)\right)$
14 12 13 ceqsalv ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={F}\left({y}\right)\to {X}\in {z}\right)↔{X}\in {F}\left({y}\right)$
15 11 14 bitri ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({F}\left({y}\right)={z}\to {X}\in {z}\right)↔{X}\in {F}\left({y}\right)$
16 15 ralbii ${⊢}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({F}\left({y}\right)={z}\to {X}\in {z}\right)↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{X}\in {F}\left({y}\right)$
17 8 16 bitr3i ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({y}\right)={z}\to {X}\in {z}\right)↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{X}\in {F}\left({y}\right)$
18 7 17 syl6bb ${⊢}\left({F}Fn{A}\wedge {B}\subseteq {A}\right)\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {F}\left[{B}\right]\to {X}\in {z}\right)↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{X}\in {F}\left({y}\right)\right)$
19 2 18 syl5bb ${⊢}\left({F}Fn{A}\wedge {B}\subseteq {A}\right)\to \left({X}\in \bigcap {F}\left[{B}\right]↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{X}\in {F}\left({y}\right)\right)$