Metamath Proof Explorer


Theorem intimafv

Description: The intersection of an image set, as an indexed intersection of function values. (Contributed by Thierry Arnoux, 15-Jun-2024)

Ref Expression
Assertion intimafv Fun F A dom F F A = x A F x

Proof

Step Hyp Ref Expression
1 dfimafn Fun F A dom F F A = y | x A F x = y
2 1 inteqd Fun F A dom F F A = y | x A F x = y
3 fvex F x V
4 3 rgenw x A F x V
5 iinabrex x A F x V x A F x = y | x A y = F x
6 4 5 ax-mp x A F x = y | x A y = F x
7 eqcom F x = y y = F x
8 7 rexbii x A F x = y x A y = F x
9 8 abbii y | x A F x = y = y | x A y = F x
10 9 inteqi y | x A F x = y = y | x A y = F x
11 6 10 eqtr4i x A F x = y | x A F x = y
12 2 11 eqtr4di Fun F A dom F F A = x A F x