![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqfnfv | Structured version Visualization version GIF version |
Description: Equality of functions is determined by their values. Special case of Exercise 4 of [TakeutiZaring] p. 28 (with domain equality omitted). (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
Ref | Expression |
---|---|
eqfnfv | ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dffn5 6391 | . . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) | |
2 | dffn5 6391 | . . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) | |
3 | eqeq12 2761 | . . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))) | |
4 | 1, 2, 3 | syl2anb 497 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))) |
5 | fvex 6350 | . . . 4 ⊢ (𝐹‘𝑥) ∈ V | |
6 | 5 | rgenw 3050 | . . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V |
7 | mpteqb 6449 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))) | |
8 | 6, 7 | ax-mp 5 | . 2 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)) |
9 | 4, 8 | syl6bb 276 | 1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1620 ∈ wcel 2127 ∀wral 3038 Vcvv 3328 ↦ cmpt 4869 Fn wfn 6032 ‘cfv 6037 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-8 2129 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 ax-sep 4921 ax-nul 4929 ax-pow 4980 ax-pr 5043 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1623 df-ex 1842 df-nf 1847 df-sb 2035 df-eu 2599 df-mo 2600 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-ral 3043 df-rex 3044 df-rab 3047 df-v 3330 df-sbc 3565 df-csb 3663 df-dif 3706 df-un 3708 df-in 3710 df-ss 3717 df-nul 4047 df-if 4219 df-sn 4310 df-pr 4312 df-op 4316 df-uni 4577 df-br 4793 df-opab 4853 df-mpt 4870 df-id 5162 df-xp 5260 df-rel 5261 df-cnv 5262 df-co 5263 df-dm 5264 df-rn 5265 df-res 5266 df-ima 5267 df-iota 6000 df-fun 6039 df-fn 6040 df-fv 6045 |
This theorem is referenced by: eqfnfv2 6463 eqfnfvd 6465 eqfnfv2f 6466 fvreseq0 6468 fnmptfvd 6471 fndmdifeq0 6474 fneqeql 6476 fnnfpeq0 6596 fconst2g 6620 cocan1 6697 cocan2 6698 weniso 6755 fnsuppres 7479 tfr3 7652 ixpfi2 8417 fipreima 8425 fseqenlem1 9008 fpwwe2lem8 9622 ofsubeq0 11180 ser0f 13019 hashgval2 13330 hashf1lem1 13402 prodf1f 14794 efcvgfsum 14986 prmreclem2 15794 1arithlem4 15803 1arith 15804 isgrpinv 17644 dprdf11 18593 psrbagconf1o 19547 islindf4 20350 pthaus 21614 xkohaus 21629 cnmpt11 21639 cnmpt21 21647 prdsxmetlem 22345 rrxmet 23362 rolle 23923 tdeglem4 23990 resinf1o 24452 dchrelbas2 25132 dchreq 25153 eqeefv 25953 axlowdimlem14 26005 nmlno0lem 27928 phoeqi 27993 occllem 28442 dfiop2 28892 hoeq 28899 ho01i 28967 hoeq1 28969 kbpj 29095 nmlnop0iALT 29134 lnopco0i 29143 nlelchi 29200 rnbra 29246 kbass5 29259 hmopidmchi 29290 hmopidmpji 29291 pjssdif2i 29313 pjinvari 29330 bnj1542 31205 bnj580 31261 subfacp1lem3 31442 subfacp1lem5 31444 mrsubff1 31689 msubff1 31731 faclimlem1 31907 fprb 31947 rdgprc 31976 broucube 33725 cocanfo 33794 eqfnun 33798 sdclem2 33820 rrnmet 33910 rrnequiv 33916 ltrnid 35893 ltrneq2 35906 tendoeq1 36523 pw2f1ocnv 38075 caofcan 38993 addrcom 39150 fsneq 39866 dvnprodlem1 40633 |
Copyright terms: Public domain | W3C validator |