Metamath Proof Explorer

Theorem fv3

Description: Alternate definition of the value of a function. Definition 6.11 of TakeutiZaring p. 26. (Contributed by NM, 30-Apr-2004) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion fv3 ⊢F⁡A=x|∃yx∈y∧AFy∧∃!yAFy

Proof

Step Hyp Ref Expression
1 elfv ⊢x∈F⁡A↔∃zx∈z∧∀yAFy↔y=z
2 biimpr ⊢AFy↔y=z→y=z→AFy
3 2 alimi ⊢∀yAFy↔y=z→∀yy=z→AFy
4 breq2 ⊢y=z→AFy↔AFz
5 4 equsalvw ⊢∀yy=z→AFy↔AFz
6 3 5 sylib ⊢∀yAFy↔y=z→AFz
7 6 anim2i ⊢x∈z∧∀yAFy↔y=z→x∈z∧AFz
8 7 eximi ⊢∃zx∈z∧∀yAFy↔y=z→∃zx∈z∧AFz
9 elequ2 ⊢z=y→x∈z↔x∈y
10 breq2 ⊢z=y→AFz↔AFy
11 9 10 anbi12d ⊢z=y→x∈z∧AFz↔x∈y∧AFy
12 11 cbvexvw ⊢∃zx∈z∧AFz↔∃yx∈y∧AFy
13 8 12 sylib ⊢∃zx∈z∧∀yAFy↔y=z→∃yx∈y∧AFy
14 exsimpr ⊢∃zx∈z∧∀yAFy↔y=z→∃z∀yAFy↔y=z
15 eu6 ⊢∃!yAFy↔∃z∀yAFy↔y=z
16 14 15 sylibr ⊢∃zx∈z∧∀yAFy↔y=z→∃!yAFy
17 13 16 jca ⊢∃zx∈z∧∀yAFy↔y=z→∃yx∈y∧AFy∧∃!yAFy
18 nfeu1 ⊢Ⅎy∃!yAFy
19 nfv ⊢Ⅎyx∈z
20 nfa1 ⊢Ⅎy∀yAFy↔y=z
21 19 20 nfan ⊢Ⅎyx∈z∧∀yAFy↔y=z
22 21 nfex ⊢Ⅎy∃zx∈z∧∀yAFy↔y=z
23 18 22 nfim ⊢Ⅎy∃!yAFy→∃zx∈z∧∀yAFy↔y=z
24 biimp ⊢AFy↔y=z→AFy→y=z
25 ax9 ⊢y=z→x∈y→x∈z
26 24 25 syl6 ⊢AFy↔y=z→AFy→x∈y→x∈z
27 26 impcomd ⊢AFy↔y=z→x∈y∧AFy→x∈z
28 27 sps ⊢∀yAFy↔y=z→x∈y∧AFy→x∈z
29 28 anc2ri ⊢∀yAFy↔y=z→x∈y∧AFy→x∈z∧∀yAFy↔y=z
30 29 com12 ⊢x∈y∧AFy→∀yAFy↔y=z→x∈z∧∀yAFy↔y=z
31 30 eximdv ⊢x∈y∧AFy→∃z∀yAFy↔y=z→∃zx∈z∧∀yAFy↔y=z
32 15 31 biimtrid ⊢x∈y∧AFy→∃!yAFy→∃zx∈z∧∀yAFy↔y=z
33 23 32 exlimi ⊢∃yx∈y∧AFy→∃!yAFy→∃zx∈z∧∀yAFy↔y=z
34 33 imp ⊢∃yx∈y∧AFy∧∃!yAFy→∃zx∈z∧∀yAFy↔y=z
35 17 34 impbii ⊢∃zx∈z∧∀yAFy↔y=z↔∃yx∈y∧AFy∧∃!yAFy
36 1 35 bitri ⊢x∈F⁡A↔∃yx∈y∧AFy∧∃!yAFy
37 36 eqabi ⊢F⁡A=x|∃yx∈y∧AFy∧∃!yAFy