fvopab5

Description: The value of a function that is expressed as an ordered pair abstraction. (Contributed by NM, 19-Feb-2006) (Revised by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypotheses	fvopab5.1	$⊢ F = \{⟨x, y⟩ \| φ\}$
	fvopab5.2	$⊢ x = A \to (φ \leftrightarrow ψ)$
Assertion	fvopab5	$⊢ A \in V \to F (A) = (ι y \| ψ)$

Proof

Step	Hyp	Ref	Expression
1		fvopab5.1	$⊢ F = \{⟨x, y⟩ \| φ\}$
2		fvopab5.2	$⊢ x = A \to (φ \leftrightarrow ψ)$
3		elex	$⊢ A \in V \to A \in V$
4		df-fv	$⊢ F (A) = (ι z \| A F z)$
5		breq2	$⊢ z = y \to (A F z \leftrightarrow A F y)$
6		nfcv	$⊢ \underline{Ⅎ} y A$
7		nfopab2	$⊢ \underline{Ⅎ} y \{⟨x, y⟩ \| φ\}$
8	1 7	nfcxfr	$⊢ \underline{Ⅎ} y F$
9		nfcv	$⊢ \underline{Ⅎ} y z$
10	6 8 9	nfbr	$⊢ Ⅎ y A F z$
11		nfv	$⊢ Ⅎ z A F y$
12	5 10 11	cbviotaw	$⊢ (ι z \| A F z) = (ι y \| A F y)$
13	4 12	eqtri	$⊢ F (A) = (ι y \| A F y)$
14		nfcv	$⊢ \underline{Ⅎ} x A$
15		nfopab1	$⊢ \underline{Ⅎ} x \{⟨x, y⟩ \| φ\}$
16	1 15	nfcxfr	$⊢ \underline{Ⅎ} x F$
17		nfcv	$⊢ \underline{Ⅎ} x y$
18	14 16 17	nfbr	$⊢ Ⅎ x A F y$
19		nfv	$⊢ Ⅎ x ψ$
20	18 19	nfbi	$⊢ Ⅎ x (A F y \leftrightarrow ψ)$
21		breq1	$⊢ x = A \to (x F y \leftrightarrow A F y)$
22	21 2	bibi12d	$⊢ x = A \to ((x F y \leftrightarrow φ) \leftrightarrow (A F y \leftrightarrow ψ))$
23		df-br	$⊢ x F y \leftrightarrow ⟨x, y⟩ \in F$
24	1	eleq2i	$⊢ ⟨x, y⟩ \in F \leftrightarrow ⟨x, y⟩ \in \{⟨x, y⟩ \| φ\}$
25		opabidw	$⊢ ⟨x, y⟩ \in \{⟨x, y⟩ \| φ\} \leftrightarrow φ$
26	23 24 25	3bitri	$⊢ x F y \leftrightarrow φ$
27	20 22 26	vtoclg1f	$⊢ A \in V \to (A F y \leftrightarrow ψ)$
28	27	iotabidv	$⊢ A \in V \to (ι y \| A F y) = (ι y \| ψ)$
29	13 28	eqtrid	$⊢ A \in V \to F (A) = (ι y \| ψ)$
30	3 29	syl	$⊢ A \in V \to F (A) = (ι y \| ψ)$

Metamath Proof Explorer

Theorem fvopab5

Proof