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 6793 | . . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) | |
2 | dffn5 6793 | . . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) | |
3 | eqeq12 2756 | . . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))) | |
4 | 1, 2, 3 | syl2anb 601 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))) |
5 | fvex 6752 | . . . 4 ⊢ (𝐹‘𝑥) ∈ V | |
6 | 5 | rgenw 3076 | . . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V |
7 | mpteqb 6859 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))) | |
8 | 6, 7 | ax-mp 5 | . 2 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)) |
9 | 4, 8 | bitrdi 290 | 1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1543 ∈ wcel 2112 ∀wral 3064 Vcvv 3423 ↦ cmpt 5152 Fn wfn 6396 ‘cfv 6401 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2710 ax-sep 5209 ax-nul 5216 ax-pr 5339 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2818 df-nfc 2889 df-ne 2944 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3425 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4255 df-if 4457 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-br 5071 df-opab 5133 df-mpt 5153 df-id 5472 df-xp 5575 df-rel 5576 df-cnv 5577 df-co 5578 df-dm 5579 df-rn 5580 df-res 5581 df-ima 5582 df-iota 6359 df-fun 6403 df-fn 6404 df-fv 6409 |
This theorem is referenced by: eqfnfv2 6875 eqfnfvd 6877 eqfnfv2f 6878 fvreseq0 6880 fnmptfvd 6883 fndmdifeq0 6886 fneqeql 6888 fnnfpeq0 7015 fprb 7031 fconst2g 7040 cocan1 7123 cocan2 7124 weniso 7185 fsplitfpar 7909 fnsuppres 7957 tfr3 8159 ixpfi2 9004 fipreima 9012 updjud 9580 fseqenlem1 9668 fpwwe2lem7 10281 ofsubeq0 11857 ser0f 13661 hashgval2 13978 hashf1lem1 14053 hashf1lem1OLD 14054 prodf1f 15489 efcvgfsum 15680 prmreclem2 16503 1arithlem4 16512 1arith 16513 smndex1n0mnd 18372 isgrpinv 18453 dprdf11 19443 frlmplusgvalb 20764 frlmvscavalb 20765 islindf4 20833 psrbagconf1o 20927 psrbagconf1oOLD 20928 pthaus 22567 xkohaus 22582 cnmpt11 22592 cnmpt21 22600 prdsxmetlem 23298 rrxmet 24337 rolle 24919 tdeglem4 24989 tdeglem4OLD 24990 resinf1o 25457 dchrelbas2 26150 dchreq 26171 eqeefv 27026 axlowdimlem14 27078 elntg2 27108 nmlno0lem 28906 phoeqi 28970 occllem 29416 dfiop2 29866 hoeq 29873 ho01i 29941 hoeq1 29943 kbpj 30069 nmlnop0iALT 30108 lnopco0i 30117 nlelchi 30174 rnbra 30220 kbass5 30233 hmopidmchi 30264 hmopidmpji 30265 pjssdif2i 30287 pjinvari 30304 bnj1542 32581 bnj580 32637 subfacp1lem3 32888 subfacp1lem5 32890 mrsubff1 33220 msubff1 33262 faclimlem1 33459 rdgprc 33520 broucube 35585 cocanfo 35650 eqfnun 35654 sdclem2 35674 rrnmet 35761 rrnequiv 35767 ltrnid 37923 ltrneq2 37936 tendoeq1 38552 sticksstones1 39866 pw2f1ocnv 40610 caofcan 41662 addrcom 41814 fsneq 42467 dvnprodlem1 43208 cfsetsnfsetf1 44271 cfsetsnfsetfo 44272 rrx2pnecoorneor 45780 rrx2linest 45807 |
Copyright terms: Public domain | W3C validator |