![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fvi | Structured version Visualization version GIF version |
Description: The value of the identity function. (Contributed by NM, 1-May-2004.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Ref | Expression |
---|---|
fvi | ⊢ (𝐴 ∈ 𝑉 → ( I ‘𝐴) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funi 6155 | . 2 ⊢ Fun I | |
2 | ididg 5508 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 I 𝐴) | |
3 | funbrfv 6480 | . 2 ⊢ (Fun I → (𝐴 I 𝐴 → ( I ‘𝐴) = 𝐴)) | |
4 | 1, 2, 3 | mpsyl 68 | 1 ⊢ (𝐴 ∈ 𝑉 → ( I ‘𝐴) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1656 ∈ wcel 2164 class class class wbr 4873 I cid 5249 Fun wfun 6117 ‘cfv 6123 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 ax-sep 5005 ax-nul 5013 ax-pr 5127 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-3an 1113 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-mo 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ral 3122 df-rex 3123 df-rab 3126 df-v 3416 df-sbc 3663 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-uni 4659 df-br 4874 df-opab 4936 df-id 5250 df-xp 5348 df-rel 5349 df-cnv 5350 df-co 5351 df-dm 5352 df-iota 6086 df-fun 6125 df-fv 6131 |
This theorem is referenced by: fviss 6503 fvmpti 6528 fvmpt2 6538 fvresi 6691 seqom0g 7817 fodomfi 8508 seqfeq4 13144 fac1 13357 facp1 13358 bcval5 13398 bcn2 13399 ids1 13657 s1val 13658 climshft2 14690 sum2id 14816 sumss 14832 prod2id 15031 fprodfac 15076 strfvi 16276 xpsc0 16573 xpsc1 16574 grpinvfvi 17817 mulgfvi 17899 efgrcl 18479 efgval 18481 frgp0 18526 frgpmhm 18531 vrgpf 18534 vrgpinv 18535 frgpupf 18539 frgpup1 18541 frgpup2 18542 frgpup3lem 18543 frgpnabllem1 18629 frgpnabllem2 18630 rlmsca2 19562 ply1basfvi 19971 ply1plusgfvi 19972 psr1sca2 19981 ply1sca2 19984 ply1scl0 20020 ply1scl1 20022 indislem 21175 2ndcctbss 21629 1stcelcls 21635 txindislem 21807 iscau3 23446 iscmet3 23461 ovolctb 23656 itg2splitlem 23914 deg1fvi 24244 deg1invg 24265 dgrle 24398 logfac 24746 ptpconn 31750 dicvscacl 37259 elinlem 38738 brfvid 38813 fvilbd 38815 |
Copyright terms: Public domain | W3C validator |