imassmpt

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	imassmpt.1	$⊢ Ⅎ x φ$
	imassmpt.2	$⊢ (φ \land x \in (A \cap C)) \to B \in V$
	imassmpt.3	$⊢ F = (x \in A ⟼ B)$
Assertion	imassmpt	$⊢ φ \to (F [C] \subseteq D \leftrightarrow \forall x \in (A \cap C) B \in D)$

Step	Hyp	Ref	Expression
1		imassmpt.1	$⊢ Ⅎ x φ$
2		imassmpt.2	$⊢ (φ \land x \in (A \cap C)) \to B \in V$
3		imassmpt.3	$⊢ F = (x \in A ⟼ B)$
4		df-ima	$⊢ F [C] = ran ({F ↾}_{C})$
5	3	reseq1i	$⊢ {F ↾}_{C} = {(x \in A ⟼ B) ↾}_{C}$
6		resmpt3	$⊢ {(x \in A ⟼ B) ↾}_{C} = (x \in (A \cap C) ⟼ B)$
7	5 6	eqtri	$⊢ {F ↾}_{C} = (x \in (A \cap C) ⟼ B)$
8	7	rneqi	$⊢ ran ({F ↾}_{C}) = ran (x \in (A \cap C) ⟼ B)$
9	4 8	eqtri	$⊢ F [C] = ran (x \in (A \cap C) ⟼ B)$
10	9	sseq1i	$⊢ F [C] \subseteq D \leftrightarrow ran (x \in (A \cap C) ⟼ B) \subseteq D$
11		eqid	$⊢ (x \in (A \cap C) ⟼ B) = (x \in (A \cap C) ⟼ B)$
12	1 11 2	rnmptssbi	$⊢ φ \to (ran (x \in (A \cap C) ⟼ B) \subseteq D \leftrightarrow \forall x \in (A \cap C) B \in D)$
13	10 12	bitrid	$⊢ φ \to (F [C] \subseteq D \leftrightarrow \forall x \in (A \cap C) B \in D)$

Metamath Proof Explorer