Metamath Proof Explorer


Theorem funimaeq

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses funimaeq.x 𝑥 𝜑
funimaeq.f ( 𝜑 → Fun 𝐹 )
funimaeq.g ( 𝜑 → Fun 𝐺 )
funimaeq.a ( 𝜑𝐴 ⊆ dom 𝐹 )
funimaeq.d ( 𝜑𝐴 ⊆ dom 𝐺 )
funimaeq.e ( ( 𝜑𝑥𝐴 ) → ( 𝐹𝑥 ) = ( 𝐺𝑥 ) )
Assertion funimaeq ( 𝜑 → ( 𝐹𝐴 ) = ( 𝐺𝐴 ) )

Proof

Step Hyp Ref Expression
1 funimaeq.x 𝑥 𝜑
2 funimaeq.f ( 𝜑 → Fun 𝐹 )
3 funimaeq.g ( 𝜑 → Fun 𝐺 )
4 funimaeq.a ( 𝜑𝐴 ⊆ dom 𝐹 )
5 funimaeq.d ( 𝜑𝐴 ⊆ dom 𝐺 )
6 funimaeq.e ( ( 𝜑𝑥𝐴 ) → ( 𝐹𝑥 ) = ( 𝐺𝑥 ) )
7 3 funfnd ( 𝜑𝐺 Fn dom 𝐺 )
8 7 adantr ( ( 𝜑𝑥𝐴 ) → 𝐺 Fn dom 𝐺 )
9 5 adantr ( ( 𝜑𝑥𝐴 ) → 𝐴 ⊆ dom 𝐺 )
10 simpr ( ( 𝜑𝑥𝐴 ) → 𝑥𝐴 )
11 fnfvima ( ( 𝐺 Fn dom 𝐺𝐴 ⊆ dom 𝐺𝑥𝐴 ) → ( 𝐺𝑥 ) ∈ ( 𝐺𝐴 ) )
12 8 9 10 11 syl3anc ( ( 𝜑𝑥𝐴 ) → ( 𝐺𝑥 ) ∈ ( 𝐺𝐴 ) )
13 6 12 eqeltrd ( ( 𝜑𝑥𝐴 ) → ( 𝐹𝑥 ) ∈ ( 𝐺𝐴 ) )
14 1 2 13 funimassd ( 𝜑 → ( 𝐹𝐴 ) ⊆ ( 𝐺𝐴 ) )
15 2 funfnd ( 𝜑𝐹 Fn dom 𝐹 )
16 15 adantr ( ( 𝜑𝑥𝐴 ) → 𝐹 Fn dom 𝐹 )
17 4 adantr ( ( 𝜑𝑥𝐴 ) → 𝐴 ⊆ dom 𝐹 )
18 fnfvima ( ( 𝐹 Fn dom 𝐹𝐴 ⊆ dom 𝐹𝑥𝐴 ) → ( 𝐹𝑥 ) ∈ ( 𝐹𝐴 ) )
19 16 17 10 18 syl3anc ( ( 𝜑𝑥𝐴 ) → ( 𝐹𝑥 ) ∈ ( 𝐹𝐴 ) )
20 6 19 eqeltrrd ( ( 𝜑𝑥𝐴 ) → ( 𝐺𝑥 ) ∈ ( 𝐹𝐴 ) )
21 1 3 20 funimassd ( 𝜑 → ( 𝐺𝐴 ) ⊆ ( 𝐹𝐴 ) )
22 14 21 eqssd ( 𝜑 → ( 𝐹𝐴 ) = ( 𝐺𝐴 ) )