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	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
	fvopab5.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	fvopab5	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 ‘ 𝐴 ) = ( ℩ 𝑦 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		fvopab5.1	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
2		fvopab5.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
4		df-fv	⊢ ( 𝐹 ‘ 𝐴 ) = ( ℩ 𝑧 𝐴 𝐹 𝑧 )
5		breq2	⊢ ( 𝑧 = 𝑦 → ( 𝐴 𝐹 𝑧 ↔ 𝐴 𝐹 𝑦 ) )
6		nfcv	⊢ Ⅎ 𝑦 𝐴
7		nfopab2	⊢ Ⅎ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
8	1 7	nfcxfr	⊢ Ⅎ 𝑦 𝐹
9		nfcv	⊢ Ⅎ 𝑦 𝑧
10	6 8 9	nfbr	⊢ Ⅎ 𝑦 𝐴 𝐹 𝑧
11		nfv	⊢ Ⅎ 𝑧 𝐴 𝐹 𝑦
12	5 10 11	cbviotaw	⊢ ( ℩ 𝑧 𝐴 𝐹 𝑧 ) = ( ℩ 𝑦 𝐴 𝐹 𝑦 )
13	4 12	eqtri	⊢ ( 𝐹 ‘ 𝐴 ) = ( ℩ 𝑦 𝐴 𝐹 𝑦 )
14		nfcv	⊢ Ⅎ 𝑥 𝐴
15		nfopab1	⊢ Ⅎ 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
16	1 15	nfcxfr	⊢ Ⅎ 𝑥 𝐹
17		nfcv	⊢ Ⅎ 𝑥 𝑦
18	14 16 17	nfbr	⊢ Ⅎ 𝑥 𝐴 𝐹 𝑦
19		nfv	⊢ Ⅎ 𝑥 𝜓
20	18 19	nfbi	⊢ Ⅎ 𝑥 ( 𝐴 𝐹 𝑦 ↔ 𝜓 )
21		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐹 𝑦 ↔ 𝐴 𝐹 𝑦 ) )
22	21 2	bibi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝐹 𝑦 ↔ 𝜑 ) ↔ ( 𝐴 𝐹 𝑦 ↔ 𝜓 ) ) )
23		df-br	⊢ ( 𝑥 𝐹 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 )
24	1	eleq2i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
25		opabidw	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜑 )
26	23 24 25	3bitri	⊢ ( 𝑥 𝐹 𝑦 ↔ 𝜑 )
27	20 22 26	vtoclg1f	⊢ ( 𝐴 ∈ V → ( 𝐴 𝐹 𝑦 ↔ 𝜓 ) )
28	27	iotabidv	⊢ ( 𝐴 ∈ V → ( ℩ 𝑦 𝐴 𝐹 𝑦 ) = ( ℩ 𝑦 𝜓 ) )
29	13 28	eqtrid	⊢ ( 𝐴 ∈ V → ( 𝐹 ‘ 𝐴 ) = ( ℩ 𝑦 𝜓 ) )
30	3 29	syl	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 ‘ 𝐴 ) = ( ℩ 𝑦 𝜓 ) )

Metamath Proof Explorer

Theorem fvopab5

Proof