mptssid

Description: The mapping operation expressed with its actual domain. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Step	Hyp	Ref	Expression
1		mptssid.1	$⊢ \underline{Ⅎ} x A$
2		mptssid.2	$⊢ C = \{x \in A \| B \in V\}$
3		eqvisset	$⊢ y = B \to B \in V$
4	3	anim2i	$⊢ (x \in A \land y = B) \to (x \in A \land B \in V)$
5		rabid	$⊢ x \in \{x \in A \| B \in V\} \leftrightarrow (x \in A \land B \in V)$
6	4 5	sylibr	$⊢ (x \in A \land y = B) \to x \in \{x \in A \| B \in V\}$
7	6 2	eleqtrrdi	$⊢ (x \in A \land y = B) \to x \in C$
8		simpr	$⊢ (x \in A \land y = B) \to y = B$
9	7 8	jca	$⊢ (x \in A \land y = B) \to (x \in C \land y = B)$
10	1	ssrab2f	$⊢ \{x \in A \| B \in V\} \subseteq A$
11	2 10	eqsstri	$⊢ C \subseteq A$
12	11	sseli	$⊢ x \in C \to x \in A$
13	12	anim1i	$⊢ (x \in C \land y = B) \to (x \in A \land y = B)$
14	9 13	impbii	$⊢ (x \in A \land y = B) \leftrightarrow (x \in C \land y = B)$
15	14	opabbii	$⊢ \{⟨x, y⟩ \| (x \in A \land y = B)\} = \{⟨x, y⟩ \| (x \in C \land y = B)\}$
16		df-mpt	$⊢ (x \in A ⟼ B) = \{⟨x, y⟩ \| (x \in A \land y = B)\}$
17		df-mpt	$⊢ (x \in C ⟼ B) = \{⟨x, y⟩ \| (x \in C \land y = B)\}$
18	15 16 17	3eqtr4i	$⊢ (x \in A ⟼ B) = (x \in C ⟼ B)$

Metamath Proof Explorer