fliftval

Description: The value of the function F . (Contributed by Mario Carneiro, 23-Dec-2016)

Step	Hyp	Ref	Expression
1		flift.1	$⊢ F = ran (x \in X ⟼ ⟨A, B⟩)$
2		flift.2	$⊢ (φ \land x \in X) \to A \in R$
3		flift.3	$⊢ (φ \land x \in X) \to B \in S$
4		fliftval.4	$⊢ x = Y \to A = C$
5		fliftval.5	$⊢ x = Y \to B = D$
6		fliftval.6	$⊢ φ \to Fun F$
7	6	adantr	$⊢ (φ \land Y \in X) \to Fun F$
8		simpr	$⊢ (φ \land Y \in X) \to Y \in X$
9		eqidd	$⊢ φ \to D = D$
10		eqidd	$⊢ Y \in X \to C = C$
11	9 10	anim12ci	$⊢ (φ \land Y \in X) \to (C = C \land D = D)$
12	4	eqeq2d	$⊢ x = Y \to (C = A \leftrightarrow C = C)$
13	5	eqeq2d	$⊢ x = Y \to (D = B \leftrightarrow D = D)$
14	12 13	anbi12d	$⊢ x = Y \to ((C = A \land D = B) \leftrightarrow (C = C \land D = D))$
15	14	rspcev	$⊢ (Y \in X \land (C = C \land D = D)) \to \exists x \in X (C = A \land D = B)$
16	8 11 15	syl2anc	$⊢ (φ \land Y \in X) \to \exists x \in X (C = A \land D = B)$
17	1 2 3	fliftel	$⊢ φ \to (C F D \leftrightarrow \exists x \in X (C = A \land D = B))$
18	17	adantr	$⊢ (φ \land Y \in X) \to (C F D \leftrightarrow \exists x \in X (C = A \land D = B))$
19	16 18	mpbird	$⊢ (φ \land Y \in X) \to C F D$
20		funbrfv	$⊢ Fun F \to (C F D \to F (C) = D)$
21	7 19 20	sylc	$⊢ (φ \land Y \in X) \to F (C) = D$

Metamath Proof Explorer