![]() |
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 6384 | . . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) | |
2 | dffn5 6384 | . . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) | |
3 | eqeq12 2784 | . . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))) | |
4 | 1, 2, 3 | syl2anb 579 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))) |
5 | fvex 6343 | . . . 4 ⊢ (𝐹‘𝑥) ∈ V | |
6 | 5 | rgenw 3073 | . . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V |
7 | mpteqb 6442 | . . 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 382 = wceq 1631 ∈ wcel 2145 ∀wral 3061 Vcvv 3351 ↦ cmpt 4864 Fn wfn 6027 ‘cfv 6032 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-sep 4916 ax-nul 4924 ax-pow 4975 ax-pr 5035 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 829 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3353 df-sbc 3589 df-csb 3684 df-dif 3727 df-un 3729 df-in 3731 df-ss 3738 df-nul 4065 df-if 4227 df-sn 4318 df-pr 4320 df-op 4324 df-uni 4576 df-br 4788 df-opab 4848 df-mpt 4865 df-id 5158 df-xp 5256 df-rel 5257 df-cnv 5258 df-co 5259 df-dm 5260 df-rn 5261 df-res 5262 df-ima 5263 df-iota 5995 df-fun 6034 df-fn 6035 df-fv 6040 |
This theorem is referenced by: eqfnfv2 6456 eqfnfvd 6458 eqfnfv2f 6459 fvreseq0 6461 fnmptfvd 6464 fndmdifeq0 6467 fneqeql 6469 fnnfpeq0 6589 fconst2g 6613 cocan1 6690 cocan2 6691 weniso 6748 fnsuppres 7475 tfr3 7649 ixpfi2 8421 fipreima 8429 updjud 8961 fseqenlem1 9048 fpwwe2lem8 9662 ofsubeq0 11220 ser0f 13062 hashgval2 13370 hashf1lem1 13442 prodf1f 14832 efcvgfsum 15023 prmreclem2 15829 1arithlem4 15838 1arith 15839 isgrpinv 17681 dprdf11 18631 psrbagconf1o 19590 islindf4 20395 pthaus 21663 xkohaus 21678 cnmpt11 21688 cnmpt21 21696 prdsxmetlem 22394 rrxmet 23411 rolle 23974 tdeglem4 24041 resinf1o 24504 dchrelbas2 25184 dchreq 25205 eqeefv 26005 axlowdimlem14 26057 nmlno0lem 27989 phoeqi 28054 occllem 28503 dfiop2 28953 hoeq 28960 ho01i 29028 hoeq1 29030 kbpj 29156 nmlnop0iALT 29195 lnopco0i 29204 nlelchi 29261 rnbra 29307 kbass5 29320 hmopidmchi 29351 hmopidmpji 29352 pjssdif2i 29374 pjinvari 29391 bnj1542 31266 bnj580 31322 subfacp1lem3 31503 subfacp1lem5 31505 mrsubff1 31750 msubff1 31792 faclimlem1 31968 fprb 32008 rdgprc 32037 broucube 33777 cocanfo 33845 eqfnun 33849 sdclem2 33871 rrnmet 33961 rrnequiv 33967 ltrnid 35944 ltrneq2 35957 tendoeq1 36574 pw2f1ocnv 38131 caofcan 39049 addrcom 39205 fsneq 39917 dvnprodlem1 40680 |
Copyright terms: Public domain | W3C validator |