![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > feq1 | Structured version Visualization version GIF version |
Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
feq1 | ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fneq1 6224 | . . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) | |
2 | rneq 5596 | . . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺) | |
3 | 2 | sseq1d 3851 | . . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵)) |
4 | 1, 3 | anbi12d 624 | . 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))) |
5 | df-f 6139 | . 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
6 | df-f 6139 | . 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)) | |
7 | 4, 5, 6 | 3bitr4g 306 | 1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 = wceq 1601 ⊆ wss 3792 ran crn 5356 Fn wfn 6130 ⟶wf 6131 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-rab 3099 df-v 3400 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-br 4887 df-opab 4949 df-rel 5362 df-cnv 5363 df-co 5364 df-dm 5365 df-rn 5366 df-fun 6137 df-fn 6138 df-f 6139 |
This theorem is referenced by: feq1d 6276 feq1i 6282 elimf 6290 f00 6337 f0bi 6338 f0dom0 6339 fconstg 6342 f1eq1 6346 fprb 6731 fconst2g 6740 fsnex 6810 elmapg 8153 ac6sfi 8492 updjud 9093 ac5num 9192 acni2 9202 cofsmo 9426 cfsmolem 9427 cfcoflem 9429 coftr 9430 alephsing 9433 axdc2lem 9605 axdc3lem2 9608 axdc3lem3 9609 axdc3 9611 axdc4lem 9612 ac6num 9636 inar1 9932 axdc4uzlem 13101 seqf1olem2 13159 seqf1o 13160 iswrd 13601 cshf1 13961 wrdlen2i 14093 ramub2 16122 ramcl 16137 isacs2 16699 isacs1i 16703 mreacs 16704 mgmb1mgm1 17640 isgrpinv 17859 isghm 18044 islindf 20555 mat1dimelbas 20682 1stcfb 21657 upxp 21835 txcn 21838 isi1f 23878 mbfi1fseqlem6 23924 mbfi1flimlem 23926 itg2addlem 23962 plyf 24391 griedg0prc 26611 isgrpo 27924 vciOLD 27988 isvclem 28004 isnvlem 28037 ajmoi 28286 ajval 28289 hlimi 28617 chlimi 28663 chcompl 28671 adjmo 29263 adjeu 29320 adjval 29321 adj1 29364 adjeq 29366 cnlnssadj 29511 pjinvari 29622 padct 30063 locfinref 30506 isrnmeas 30861 orderseqlem 32341 soseq 32343 elno 32388 filnetlem4 32964 bj-finsumval0 33749 poimirlem25 34060 poimirlem28 34063 volsupnfl 34080 mbfresfi 34081 upixp 34149 sdclem2 34162 sdclem1 34163 fdc 34165 ismgmOLD 34273 elghomlem2OLD 34309 istendo 36914 ismrc 38224 fmuldfeqlem1 40722 fmuldfeq 40723 dvnprodlem1 41089 stoweidlem15 41159 stoweidlem16 41160 stoweidlem17 41161 stoweidlem19 41163 stoweidlem20 41164 stoweidlem21 41165 stoweidlem22 41166 stoweidlem23 41167 stoweidlem27 41171 stoweidlem31 41175 stoweidlem32 41176 stoweidlem42 41186 stoweidlem48 41192 stoweidlem51 41195 stoweidlem59 41203 isomenndlem 41671 smfpimcclem 41940 lincdifsn 43228 |
Copyright terms: Public domain | W3C validator |