Theorem opabiotafun

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

	Ref	Expression
Hypothesis	opabiota.1	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑦 ∣ 𝜑 } = { 𝑦 } }
Assertion	opabiotafun	⊢ Fun 𝐹

Proof

Step	Hyp	Ref	Expression
1		opabiota.1	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑦 ∣ 𝜑 } = { 𝑦 } }
2		funopab	⊢ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑦 ∣ 𝜑 } = { 𝑦 } } ↔ ∀ 𝑥 ∃* 𝑦 { 𝑦 ∣ 𝜑 } = { 𝑦 } )
3		mo2icl	⊢ ( ∀ 𝑧 ( { 𝑦 ∣ 𝜑 } = { 𝑧 } → 𝑧 = ∪ { 𝑦 ∣ 𝜑 } ) → ∃* 𝑧 { 𝑦 ∣ 𝜑 } = { 𝑧 } )
4		unieq	⊢ ( { 𝑦 ∣ 𝜑 } = { 𝑧 } → ∪ { 𝑦 ∣ 𝜑 } = ∪ { 𝑧 } )
5		unisnv	⊢ ∪ { 𝑧 } = 𝑧
6	4 5	eqtr2di	⊢ ( { 𝑦 ∣ 𝜑 } = { 𝑧 } → 𝑧 = ∪ { 𝑦 ∣ 𝜑 } )
7	3 6	mpg	⊢ ∃* 𝑧 { 𝑦 ∣ 𝜑 } = { 𝑧 }
8		nfv	⊢ Ⅎ 𝑧 { 𝑦 ∣ 𝜑 } = { 𝑦 }
9		nfab1	⊢ Ⅎ 𝑦 { 𝑦 ∣ 𝜑 }
10	9	nfeq1	⊢ Ⅎ 𝑦 { 𝑦 ∣ 𝜑 } = { 𝑧 }
11		sneq	⊢ ( 𝑦 = 𝑧 → { 𝑦 } = { 𝑧 } )
12	11	eqeq2d	⊢ ( 𝑦 = 𝑧 → ( { 𝑦 ∣ 𝜑 } = { 𝑦 } ↔ { 𝑦 ∣ 𝜑 } = { 𝑧 } ) )
13	8 10 12	cbvmow	⊢ ( ∃* 𝑦 { 𝑦 ∣ 𝜑 } = { 𝑦 } ↔ ∃* 𝑧 { 𝑦 ∣ 𝜑 } = { 𝑧 } )
14	7 13	mpbir	⊢ ∃* 𝑦 { 𝑦 ∣ 𝜑 } = { 𝑦 }
15	2 14	mpgbir	⊢ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑦 ∣ 𝜑 } = { 𝑦 } }
16	1	funeqi	⊢ ( Fun 𝐹 ↔ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑦 ∣ 𝜑 } = { 𝑦 } } )
17	15 16	mpbir	⊢ Fun 𝐹