Metamath Proof Explorer

Theorem fvopab6

Description: Value of a function given by ordered-pair class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 11-Sep-2015)

		Ref	Expression
	Hypotheses	fvopab6.1	$⊢ F = \{⟨x, y⟩ \| (φ \land y = B)\}$
		fvopab6.2	$⊢ x = A \to (φ \leftrightarrow ψ)$
		fvopab6.3	$⊢ x = A \to B = C$
	Assertion	fvopab6	$⊢ (A \in D \land C \in R \land ψ) \to F (A) = C$

Proof

Step	Hyp	Ref	Expression
1		fvopab6.1	$⊢ F = \{⟨x, y⟩ \| (φ \land y = B)\}$
2		fvopab6.2	$⊢ x = A \to (φ \leftrightarrow ψ)$
3		fvopab6.3	$⊢ x = A \to B = C$
4		elex	$⊢ A \in D \to A \in V$
5	3	eqeq2d	$⊢ x = A \to (y = B \leftrightarrow y = C)$
6	2 5	anbi12d	$⊢ x = A \to ((φ \land y = B) \leftrightarrow (ψ \land y = C))$
7		iba	$⊢ y = C \to (ψ \leftrightarrow (ψ \land y = C))$
8	7	bicomd	$⊢ y = C \to ((ψ \land y = C) \leftrightarrow ψ)$
9		moeq	$⊢ \exists^{*} y y = B$
10	9	moani	$⊢ \exists^{*} y (φ \land y = B)$
11	10	a1i	$⊢ x \in V \to \exists^{*} y (φ \land y = B)$
12		vex	$⊢ x \in V$
13	12	biantrur	$⊢ (φ \land y = B) \leftrightarrow (x \in V \land (φ \land y = B))$
14	13	opabbii	$⊢ \{⟨x, y⟩ \| (φ \land y = B)\} = \{⟨x, y⟩ \| (x \in V \land (φ \land y = B))\}$
15	1 14	eqtri	$⊢ F = \{⟨x, y⟩ \| (x \in V \land (φ \land y = B))\}$
16	6 8 11 15	fvopab3ig	$⊢ (A \in V \land C \in R) \to (ψ \to F (A) = C)$
17	4 16	sylan	$⊢ (A \in D \land C \in R) \to (ψ \to F (A) = C)$
18	17	3impia	$⊢ (A \in D \land C \in R \land ψ) \to F (A) = C$