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 FunFAdomFFA=xAFx

Proof

Step Hyp Ref Expression
1 dfimafn FunFAdomFFA=y|xAFx=y
2 1 inteqd FunFAdomFFA=y|xAFx=y
3 fvex FxV
4 3 rgenw xAFxV
5 iinabrex xAFxVxAFx=y|xAy=Fx
6 4 5 ax-mp xAFx=y|xAy=Fx
7 eqcom Fx=yy=Fx
8 7 rexbii xAFx=yxAy=Fx
9 8 abbii y|xAFx=y=y|xAy=Fx
10 9 inteqi y|xAFx=y=y|xAy=Fx
11 6 10 eqtr4i xAFx=y|xAFx=y
12 2 11 eqtr4di FunFAdomFFA=xAFx