Theorem opabiotadm

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

	Ref	Expression
Hypothesis	opabiota.1	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑦 ∣ 𝜑 } = { 𝑦 } }
Assertion	opabiotadm	⊢ dom 𝐹 = { 𝑥 ∣ ∃! 𝑦 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		opabiota.1	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑦 ∣ 𝜑 } = { 𝑦 } }
2		dmopab	⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑦 ∣ 𝜑 } = { 𝑦 } } = { 𝑥 ∣ ∃ 𝑦 { 𝑦 ∣ 𝜑 } = { 𝑦 } }
3	1	dmeqi	⊢ dom 𝐹 = dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑦 ∣ 𝜑 } = { 𝑦 } }
4		euabsn	⊢ ( ∃! 𝑦 𝜑 ↔ ∃ 𝑦 { 𝑦 ∣ 𝜑 } = { 𝑦 } )
5	4	abbii	⊢ { 𝑥 ∣ ∃! 𝑦 𝜑 } = { 𝑥 ∣ ∃ 𝑦 { 𝑦 ∣ 𝜑 } = { 𝑦 } }
6	2 3 5	3eqtr4i	⊢ dom 𝐹 = { 𝑥 ∣ ∃! 𝑦 𝜑 }