Theorem fnopabg

Description: Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 30-Jan-2004) (Proof shortened by Mario Carneiro, 4-Dec-2016)

	Ref	Expression
Hypothesis	fnopabg.1	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
Assertion	fnopabg	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝜑 ↔ 𝐹 Fn 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fnopabg.1	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
2		moanimv	⊢ ( ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝜑 ) )
3	2	albii	⊢ ( ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝜑 ) )
4		funopab	⊢ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ↔ ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
5		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝜑 ) )
6	3 4 5	3bitr4ri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝜑 ↔ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } )
7		dmopab3	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝜑 ↔ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = 𝐴 )
8	6 7	anbi12i	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝜑 ) ↔ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∧ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = 𝐴 ) )
9		r19.26	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∃* 𝑦 𝜑 ∧ ∃ 𝑦 𝜑 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝜑 ) )
10		df-fn	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } Fn 𝐴 ↔ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∧ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = 𝐴 ) )
11	8 9 10	3bitr4i	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∃* 𝑦 𝜑 ∧ ∃ 𝑦 𝜑 ) ↔ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } Fn 𝐴 )
12		df-eu	⊢ ( ∃! 𝑦 𝜑 ↔ ( ∃ 𝑦 𝜑 ∧ ∃* 𝑦 𝜑 ) )
13	12	biancomi	⊢ ( ∃! 𝑦 𝜑 ↔ ( ∃* 𝑦 𝜑 ∧ ∃ 𝑦 𝜑 ) )
14	13	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ( ∃* 𝑦 𝜑 ∧ ∃ 𝑦 𝜑 ) )
15	1	fneq1i	⊢ ( 𝐹 Fn 𝐴 ↔ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } Fn 𝐴 )
16	11 14 15	3bitr4i	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝜑 ↔ 𝐹 Fn 𝐴 )