funimaeq

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

Step	Hyp	Ref	Expression
1		funimaeq.x	$⊢ Ⅎ x φ$
2		funimaeq.f	$⊢ φ \to Fun F$
3		funimaeq.g	$⊢ φ \to Fun G$
4		funimaeq.a	$⊢ φ \to A \subseteq dom F$
5		funimaeq.d	$⊢ φ \to A \subseteq dom G$
6		funimaeq.e	$⊢ (φ \land x \in A) \to F (x) = G (x)$
7	3	funfnd	$⊢ φ \to G Fn dom G$
8	7	adantr	$⊢ (φ \land x \in A) \to G Fn dom G$
9	5	adantr	$⊢ (φ \land x \in A) \to A \subseteq dom G$
10		simpr	$⊢ (φ \land x \in A) \to x \in A$
11		fnfvima	$⊢ (G Fn dom G \land A \subseteq dom G \land x \in A) \to G (x) \in G [A]$
12	8 9 10 11	syl3anc	$⊢ (φ \land x \in A) \to G (x) \in G [A]$
13	6 12	eqeltrd	$⊢ (φ \land x \in A) \to F (x) \in G [A]$
14	1 2 13	funimassd	$⊢ φ \to F [A] \subseteq G [A]$
15	2	funfnd	$⊢ φ \to F Fn dom F$
16	15	adantr	$⊢ (φ \land x \in A) \to F Fn dom F$
17	4	adantr	$⊢ (φ \land x \in A) \to A \subseteq dom F$
18		fnfvima	$⊢ (F Fn dom F \land A \subseteq dom F \land x \in A) \to F (x) \in F [A]$
19	16 17 10 18	syl3anc	$⊢ (φ \land x \in A) \to F (x) \in F [A]$
20	6 19	eqeltrrd	$⊢ (φ \land x \in A) \to G (x) \in F [A]$
21	1 3 20	funimassd	$⊢ φ \to G [A] \subseteq F [A]$
22	14 21	eqssd	$⊢ φ \to F [A] = G [A]$

Metamath Proof Explorer