![]() |
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 6960 | . . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) | |
2 | dffn5 6960 | . . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) | |
3 | eqeq12 2744 | . . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))) | |
4 | 1, 2, 3 | syl2anb 596 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))) |
5 | fvex 6913 | . . . 4 ⊢ (𝐹‘𝑥) ∈ V | |
6 | 5 | rgenw 3061 | . . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V |
7 | mpteqb 7027 | . . 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 394 = wceq 1533 ∈ wcel 2098 ∀wral 3057 Vcvv 3471 ↦ cmpt 5233 Fn wfn 6546 ‘cfv 6551 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2698 ax-sep 5301 ax-nul 5308 ax-pr 5431 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ne 2937 df-ral 3058 df-rex 3067 df-rab 3429 df-v 3473 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4325 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4911 df-br 5151 df-opab 5213 df-mpt 5234 df-id 5578 df-xp 5686 df-rel 5687 df-cnv 5688 df-co 5689 df-dm 5690 df-rn 5691 df-res 5692 df-ima 5693 df-iota 6503 df-fun 6553 df-fn 6554 df-fv 6559 |
This theorem is referenced by: eqfnfv2 7044 eqfnfvd 7046 eqfnfv2f 7047 eqfnun 7049 fvreseq0 7050 fnmptfvd 7053 fndmdifeq0 7056 fneqeql 7058 fnnfpeq0 7191 fprb 7210 fconst2g 7219 cocan1 7304 cocan2 7305 weniso 7366 fsplitfpar 8127 fnsuppres 8200 tfr3 8424 ixpfi2 9380 fipreima 9388 updjud 9963 fseqenlem1 10053 fpwwe2lem7 10666 ofsubeq0 12245 ser0f 14058 hashgval2 14375 hashf1lem1 14453 hashf1lem1OLD 14454 prodf1f 15876 efcvgfsum 16068 prmreclem2 16891 1arithlem4 16900 1arith 16901 smndex1n0mnd 18869 isgrpinv 18955 dprdf11 19985 frlmplusgvalb 21708 frlmvscavalb 21709 islindf4 21777 psrbagconf1o 21875 psrbagconf1oOLD 21876 pthaus 23560 xkohaus 23575 cnmpt11 23585 cnmpt21 23593 prdsxmetlem 24292 rrxmet 25354 rolle 25940 tdeglem4 26013 tdeglem4OLD 26014 resinf1o 26488 dchrelbas2 27188 dchreq 27209 eqeefv 28732 axlowdimlem14 28784 elntg2 28814 nmlno0lem 30621 phoeqi 30685 occllem 31131 dfiop2 31581 hoeq 31588 ho01i 31656 hoeq1 31658 kbpj 31784 nmlnop0iALT 31823 lnopco0i 31832 nlelchi 31889 rnbra 31935 kbass5 31948 hmopidmchi 31979 hmopidmpji 31980 pjssdif2i 32002 pjinvari 32019 bnj1542 34493 bnj580 34549 subfacp1lem3 34797 subfacp1lem5 34799 mrsubff1 35129 msubff1 35171 faclimlem1 35342 rdgprc 35395 broucube 37132 cocanfo 37197 sdclem2 37220 rrnmet 37307 rrnequiv 37313 ltrnid 39612 ltrneq2 39625 tendoeq1 40241 sticksstones1 41622 pw2f1ocnv 42461 caofcan 43763 addrcom 43915 fsneq 44582 dvnprodlem1 45336 cfsetsnfsetf1 46443 cfsetsnfsetfo 46444 rrx2pnecoorneor 47839 rrx2linest 47866 |
Copyright terms: Public domain | W3C validator |