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 F Fn A B A X F B y B X F y

Proof

Step Hyp Ref Expression
1 elintfv.1 X V
2 1 elint X F B z z F B X z
3 fvelimab F Fn A B A z F B y B F y = z
4 3 imbi1d F Fn A B A z F B X z y B F y = z X z
5 r19.23v y B F y = z X z y B F y = z X z
6 4 5 bitr4di F Fn A B A z F B X z y B F y = z X z
7 6 albidv F Fn A B A z z F B X z z y B F y = z X z
8 ralcom4 y B z F y = z X z z y B F 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 z F y = z X z z z = F y X z
12 fvex F y V
13 eleq2 z = F y X z X F y
14 12 13 ceqsalv z z = F y X z X F y
15 11 14 bitri z F y = z X z X F y
16 15 ralbii y B z F y = z X z y B X F y
17 8 16 bitr3i z y B F y = z X z y B X F y
18 7 17 bitrdi F Fn A B A z z F B X z y B X F y
19 2 18 syl5bb F Fn A B A X F B y B X F y