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		vex	⊢ 𝑧 ∈ V
6	5	unisn	⊢ ∪ { 𝑧 } = 𝑧
7	4 6	eqtr2di	⊢ ( { 𝑦 ∣ 𝜑 } = { 𝑧 } → 𝑧 = ∪ { 𝑦 ∣ 𝜑 } )
8	3 7	mpg	⊢ ∃* 𝑧 { 𝑦 ∣ 𝜑 } = { 𝑧 }
9		nfv	⊢ Ⅎ 𝑧 { 𝑦 ∣ 𝜑 } = { 𝑦 }
10		nfab1	⊢ Ⅎ 𝑦 { 𝑦 ∣ 𝜑 }
11	10	nfeq1	⊢ Ⅎ 𝑦 { 𝑦 ∣ 𝜑 } = { 𝑧 }
12		sneq	⊢ ( 𝑦 = 𝑧 → { 𝑦 } = { 𝑧 } )
13	12	eqeq2d	⊢ ( 𝑦 = 𝑧 → ( { 𝑦 ∣ 𝜑 } = { 𝑦 } ↔ { 𝑦 ∣ 𝜑 } = { 𝑧 } ) )
14	9 11 13	cbvmow	⊢ ( ∃* 𝑦 { 𝑦 ∣ 𝜑 } = { 𝑦 } ↔ ∃* 𝑧 { 𝑦 ∣ 𝜑 } = { 𝑧 } )
15	8 14	mpbir	⊢ ∃* 𝑦 { 𝑦 ∣ 𝜑 } = { 𝑦 }
16	2 15	mpgbir	⊢ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑦 ∣ 𝜑 } = { 𝑦 } }
17	1	funeqi	⊢ ( Fun 𝐹 ↔ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑦 ∣ 𝜑 } = { 𝑦 } } )
18	16 17	mpbir	⊢ Fun 𝐹