![]() |
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 6950 | . . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) | |
2 | dffn5 6950 | . . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) | |
3 | eqeq12 2749 | . . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))) | |
4 | 1, 2, 3 | syl2anb 598 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))) |
5 | fvex 6904 | . . . 4 ⊢ (𝐹‘𝑥) ∈ V | |
6 | 5 | rgenw 3065 | . . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V |
7 | mpteqb 7017 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))) | |
8 | 6, 7 | ax-mp 5 | . 2 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)) |
9 | 4, 8 | bitrdi 286 | 1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∀wral 3061 Vcvv 3474 ↦ cmpt 5231 Fn wfn 6538 ‘cfv 6543 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-sep 5299 ax-nul 5306 ax-pr 5427 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3433 df-v 3476 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-iota 6495 df-fun 6545 df-fn 6546 df-fv 6551 |
This theorem is referenced by: eqfnfv2 7033 eqfnfvd 7035 eqfnfv2f 7036 eqfnun 7038 fvreseq0 7039 fnmptfvd 7042 fndmdifeq0 7045 fneqeql 7047 fnnfpeq0 7178 fprb 7197 fconst2g 7206 cocan1 7291 cocan2 7292 weniso 7353 fsplitfpar 8106 fnsuppres 8178 tfr3 8401 ixpfi2 9352 fipreima 9360 updjud 9931 fseqenlem1 10021 fpwwe2lem7 10634 ofsubeq0 12213 ser0f 14025 hashgval2 14342 hashf1lem1 14419 hashf1lem1OLD 14420 prodf1f 15842 efcvgfsum 16033 prmreclem2 16854 1arithlem4 16863 1arith 16864 smndex1n0mnd 18829 isgrpinv 18914 dprdf11 19934 frlmplusgvalb 21543 frlmvscavalb 21544 islindf4 21612 psrbagconf1o 21708 psrbagconf1oOLD 21709 pthaus 23362 xkohaus 23377 cnmpt11 23387 cnmpt21 23395 prdsxmetlem 24094 rrxmet 25149 rolle 25731 tdeglem4 25801 tdeglem4OLD 25802 resinf1o 26269 dchrelbas2 26964 dchreq 26985 eqeefv 28416 axlowdimlem14 28468 elntg2 28498 nmlno0lem 30301 phoeqi 30365 occllem 30811 dfiop2 31261 hoeq 31268 ho01i 31336 hoeq1 31338 kbpj 31464 nmlnop0iALT 31503 lnopco0i 31512 nlelchi 31569 rnbra 31615 kbass5 31628 hmopidmchi 31659 hmopidmpji 31660 pjssdif2i 31682 pjinvari 31699 bnj1542 34154 bnj580 34210 subfacp1lem3 34459 subfacp1lem5 34461 mrsubff1 34791 msubff1 34833 faclimlem1 35005 rdgprc 35058 broucube 36825 cocanfo 36890 sdclem2 36913 rrnmet 37000 rrnequiv 37006 ltrnid 39309 ltrneq2 39322 tendoeq1 39938 sticksstones1 41268 pw2f1ocnv 42078 caofcan 43384 addrcom 43536 fsneq 44204 dvnprodlem1 44961 cfsetsnfsetf1 46068 cfsetsnfsetfo 46069 rrx2pnecoorneor 47489 rrx2linest 47516 |
Copyright terms: Public domain | W3C validator |