Metamath Proof Explorer

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 ⊢FdefAtA↔A∈dom⁡F∧∃!yAFy

Proof

Step Hyp Ref Expression
1 df-dfat ⊢FdefAtA↔A∈dom⁡F∧Fun⁡F↾A
2 relres ⊢Rel⁡F↾A
3 dffun8 ⊢Fun⁡F↾A↔Rel⁡F↾A∧∀x∈dom⁡F↾A∃!yxF↾Ay
4 2 3 mpbiran ⊢Fun⁡F↾A↔∀x∈dom⁡F↾A∃!yxF↾Ay
5 4 anbi2i ⊢A∈dom⁡F∧Fun⁡F↾A↔A∈dom⁡F∧∀x∈dom⁡F↾A∃!yxF↾Ay
6 brres ⊢y∈V→xF↾Ay↔x∈A∧xFy
7 6 elv ⊢xF↾Ay↔x∈A∧xFy
8 7 a1i ⊢A∈dom⁡F→xF↾Ay↔x∈A∧xFy
9 8 eubidv ⊢A∈dom⁡F→∃!yxF↾Ay↔∃!yx∈A∧xFy
10 9 ralbidv ⊢A∈dom⁡F→∀x∈dom⁡F↾A∃!yxF↾Ay↔∀x∈dom⁡F↾A∃!yx∈A∧xFy
11 eldmressnsn ⊢A∈dom⁡F→A∈dom⁡F↾A
12 eldmressn ⊢x∈dom⁡F↾A→x=A
13 velsn ⊢x∈A↔x=A
14 13 biimpri ⊢x=A→x∈A
15 breq1 ⊢x=A→xFy↔AFy
16 15 anbi2d ⊢x=A→x∈A∧xFy↔x∈A∧AFy
17 14 16 mpbirand ⊢x=A→x∈A∧xFy↔AFy
18 17 eubidv ⊢x=A→∃!yx∈A∧xFy↔∃!yAFy
19 11 12 18 ralbinrald ⊢A∈dom⁡F→∀x∈dom⁡F↾A∃!yx∈A∧xFy↔∃!yAFy
20 10 19 bitrd ⊢A∈dom⁡F→∀x∈dom⁡F↾A∃!yxF↾Ay↔∃!yAFy
21 20 pm5.32i ⊢A∈dom⁡F∧∀x∈dom⁡F↾A∃!yxF↾Ay↔A∈dom⁡F∧∃!yAFy
22 1 5 21 3bitri ⊢FdefAtA↔A∈dom⁡F∧∃!yAFy