Theorem dfdfat2

Description: Alternate definition of the predicate "defined at" not using the Fun predicate. (Contributed by Alexander van der Vekens, 22-Jul-2017) (Proof shortened by Peter Mazsa, 2-Oct-2022)

	Ref	Expression
Assertion	dfdfat2	⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑦 𝐴 𝐹 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		df-dfat	⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
2		relres	⊢ Rel ( 𝐹 ↾ { 𝐴 } )
3		dffun8	⊢ ( Fun ( 𝐹 ↾ { 𝐴 } ) ↔ ( Rel ( 𝐹 ↾ { 𝐴 } ) ∧ ∀ 𝑥 ∈ dom ( 𝐹 ↾ { 𝐴 } ) ∃! 𝑦 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ) )
4	2 3	mpbiran	⊢ ( Fun ( 𝐹 ↾ { 𝐴 } ) ↔ ∀ 𝑥 ∈ dom ( 𝐹 ↾ { 𝐴 } ) ∃! 𝑦 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 )
5	4	anbi2i	⊢ ( ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ↔ ( 𝐴 ∈ dom 𝐹 ∧ ∀ 𝑥 ∈ dom ( 𝐹 ↾ { 𝐴 } ) ∃! 𝑦 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ) )
6		brres	⊢ ( 𝑦 ∈ V → ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ↔ ( 𝑥 ∈ { 𝐴 } ∧ 𝑥 𝐹 𝑦 ) ) )
7	6	elv	⊢ ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ↔ ( 𝑥 ∈ { 𝐴 } ∧ 𝑥 𝐹 𝑦 ) )
8	7	a1i	⊢ ( 𝐴 ∈ dom 𝐹 → ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ↔ ( 𝑥 ∈ { 𝐴 } ∧ 𝑥 𝐹 𝑦 ) ) )
9	8	eubidv	⊢ ( 𝐴 ∈ dom 𝐹 → ( ∃! 𝑦 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ↔ ∃! 𝑦 ( 𝑥 ∈ { 𝐴 } ∧ 𝑥 𝐹 𝑦 ) ) )
10	9	ralbidv	⊢ ( 𝐴 ∈ dom 𝐹 → ( ∀ 𝑥 ∈ dom ( 𝐹 ↾ { 𝐴 } ) ∃! 𝑦 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ↔ ∀ 𝑥 ∈ dom ( 𝐹 ↾ { 𝐴 } ) ∃! 𝑦 ( 𝑥 ∈ { 𝐴 } ∧ 𝑥 𝐹 𝑦 ) ) )
11		eldmressnsn	⊢ ( 𝐴 ∈ dom 𝐹 → 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) )
12		eldmressn	⊢ ( 𝑥 ∈ dom ( 𝐹 ↾ { 𝐴 } ) → 𝑥 = 𝐴 )
13		velsn	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
14	13	biimpri	⊢ ( 𝑥 = 𝐴 → 𝑥 ∈ { 𝐴 } )
15		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐹 𝑦 ↔ 𝐴 𝐹 𝑦 ) )
16	15	anbi2d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑥 𝐹 𝑦 ) ↔ ( 𝑥 ∈ { 𝐴 } ∧ 𝐴 𝐹 𝑦 ) ) )
17	14 16	mpbirand	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑥 𝐹 𝑦 ) ↔ 𝐴 𝐹 𝑦 ) )
18	17	eubidv	⊢ ( 𝑥 = 𝐴 → ( ∃! 𝑦 ( 𝑥 ∈ { 𝐴 } ∧ 𝑥 𝐹 𝑦 ) ↔ ∃! 𝑦 𝐴 𝐹 𝑦 ) )
19	11 12 18	ralbinrald	⊢ ( 𝐴 ∈ dom 𝐹 → ( ∀ 𝑥 ∈ dom ( 𝐹 ↾ { 𝐴 } ) ∃! 𝑦 ( 𝑥 ∈ { 𝐴 } ∧ 𝑥 𝐹 𝑦 ) ↔ ∃! 𝑦 𝐴 𝐹 𝑦 ) )
20	10 19	bitrd	⊢ ( 𝐴 ∈ dom 𝐹 → ( ∀ 𝑥 ∈ dom ( 𝐹 ↾ { 𝐴 } ) ∃! 𝑦 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ↔ ∃! 𝑦 𝐴 𝐹 𝑦 ) )
21	20	pm5.32i	⊢ ( ( 𝐴 ∈ dom 𝐹 ∧ ∀ 𝑥 ∈ dom ( 𝐹 ↾ { 𝐴 } ) ∃! 𝑦 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ) ↔ ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑦 𝐴 𝐹 𝑦 ) )
22	1 5 21	3bitri	⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑦 𝐴 𝐹 𝑦 ) )