Theorem opabiota

Description: Define a function whose value is "the unique y such that ph ( x , y ) ". (Contributed by NM, 16-Nov-2013)

	Ref	Expression
Hypotheses	opabiota.1	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑦 ∣ 𝜑 } = { 𝑦 } }
	opabiota.2	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
Assertion	opabiota	⊢ ( 𝐵 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐵 ) = ( ℩ 𝑦 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		opabiota.1	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑦 ∣ 𝜑 } = { 𝑦 } }
2		opabiota.2	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
3		fveq2	⊢ ( 𝑥 = 𝐵 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) )
4	2	iotabidv	⊢ ( 𝑥 = 𝐵 → ( ℩ 𝑦 𝜑 ) = ( ℩ 𝑦 𝜓 ) )
5	3 4	eqeq12d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐹 ‘ 𝑥 ) = ( ℩ 𝑦 𝜑 ) ↔ ( 𝐹 ‘ 𝐵 ) = ( ℩ 𝑦 𝜓 ) ) )
6		vex	⊢ 𝑥 ∈ V
7	6	eldm	⊢ ( 𝑥 ∈ dom 𝐹 ↔ ∃ 𝑦 𝑥 𝐹 𝑦 )
8		nfiota1	⊢ Ⅎ 𝑦 ( ℩ 𝑦 𝜑 )
9	8	nfeq2	⊢ Ⅎ 𝑦 ( 𝐹 ‘ 𝑥 ) = ( ℩ 𝑦 𝜑 )
10	1	opabiotafun	⊢ Fun 𝐹
11		funbrfv	⊢ ( Fun 𝐹 → ( 𝑥 𝐹 𝑦 → ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
12	10 11	ax-mp	⊢ ( 𝑥 𝐹 𝑦 → ( 𝐹 ‘ 𝑥 ) = 𝑦 )
13		df-br	⊢ ( 𝑥 𝐹 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 )
14	1	eleq2i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑦 ∣ 𝜑 } = { 𝑦 } } )
15		opabidw	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑦 ∣ 𝜑 } = { 𝑦 } } ↔ { 𝑦 ∣ 𝜑 } = { 𝑦 } )
16	13 14 15	3bitri	⊢ ( 𝑥 𝐹 𝑦 ↔ { 𝑦 ∣ 𝜑 } = { 𝑦 } )
17		vsnid	⊢ 𝑦 ∈ { 𝑦 }
18		id	⊢ ( { 𝑦 ∣ 𝜑 } = { 𝑦 } → { 𝑦 ∣ 𝜑 } = { 𝑦 } )
19	17 18	eleqtrrid	⊢ ( { 𝑦 ∣ 𝜑 } = { 𝑦 } → 𝑦 ∈ { 𝑦 ∣ 𝜑 } )
20		abid	⊢ ( 𝑦 ∈ { 𝑦 ∣ 𝜑 } ↔ 𝜑 )
21	19 20	sylib	⊢ ( { 𝑦 ∣ 𝜑 } = { 𝑦 } → 𝜑 )
22	16 21	sylbi	⊢ ( 𝑥 𝐹 𝑦 → 𝜑 )
23		vex	⊢ 𝑦 ∈ V
24	6 23	breldm	⊢ ( 𝑥 𝐹 𝑦 → 𝑥 ∈ dom 𝐹 )
25	1	opabiotadm	⊢ dom 𝐹 = { 𝑥 ∣ ∃! 𝑦 𝜑 }
26	25	abeq2i	⊢ ( 𝑥 ∈ dom 𝐹 ↔ ∃! 𝑦 𝜑 )
27	24 26	sylib	⊢ ( 𝑥 𝐹 𝑦 → ∃! 𝑦 𝜑 )
28		iota1	⊢ ( ∃! 𝑦 𝜑 → ( 𝜑 ↔ ( ℩ 𝑦 𝜑 ) = 𝑦 ) )
29	27 28	syl	⊢ ( 𝑥 𝐹 𝑦 → ( 𝜑 ↔ ( ℩ 𝑦 𝜑 ) = 𝑦 ) )
30	22 29	mpbid	⊢ ( 𝑥 𝐹 𝑦 → ( ℩ 𝑦 𝜑 ) = 𝑦 )
31	12 30	eqtr4d	⊢ ( 𝑥 𝐹 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( ℩ 𝑦 𝜑 ) )
32	9 31	exlimi	⊢ ( ∃ 𝑦 𝑥 𝐹 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( ℩ 𝑦 𝜑 ) )
33	7 32	sylbi	⊢ ( 𝑥 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑥 ) = ( ℩ 𝑦 𝜑 ) )
34	5 33	vtoclga	⊢ ( 𝐵 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐵 ) = ( ℩ 𝑦 𝜓 ) )