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 5893 | . . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) | |
2 | rneq 5272 | . . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺) | |
3 | 2 | sseq1d 3595 | . . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵)) |
4 | 1, 3 | anbi12d 743 | . 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))) |
5 | df-f 5808 | . 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
6 | df-f 5808 | . 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)) | |
7 | 4, 5, 6 | 3bitr4g 302 | 1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ⊆ wss 3540 ran crn 5039 Fn wfn 5799 ⟶wf 5800 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-br 4584 df-opab 4644 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-fun 5806 df-fn 5807 df-f 5808 |
This theorem is referenced by: feq1d 5943 feq1i 5949 elimf 5957 f00 6000 f0bi 6001 f0dom0 6002 fconstg 6005 f1eq1 6009 fconst2g 6373 fsnex 6438 elmapg 7757 ac6sfi 8089 ac5num 8742 acni2 8752 cofsmo 8974 cfsmolem 8975 cfcoflem 8977 coftr 8978 alephsing 8981 axdc2lem 9153 axdc3lem2 9156 axdc3lem3 9157 axdc3 9159 axdc4lem 9160 ac6num 9184 inar1 9476 axdc4uzlem 12644 seqf1olem2 12703 seqf1o 12704 iswrd 13162 cshf1 13407 wrdlen2i 13534 ramub2 15556 ramcl 15571 isacs2 16137 isacs1i 16141 mreacs 16142 mgmb1mgm1 17077 isgrpinv 17295 isghm 17483 islindf 19970 mat1dimelbas 20096 1stcfb 21058 upxp 21236 txcn 21239 isi1f 23247 mbfi1fseqlem6 23293 mbfi1flimlem 23295 itg2addlem 23331 plyf 23758 wlkelwrd 26058 iseupa 26492 isgrpo 26735 vciOLD 26800 isvclem 26816 isnvlem 26849 ajmoi 27098 ajval 27101 hlimi 27429 chlimi 27475 chcompl 27483 adjmo 28075 adjeu 28132 adjval 28133 adj1 28176 adjeq 28178 cnlnssadj 28323 pjinvari 28434 padct 28885 locfinref 29236 isrnmeas 29590 fprb 30916 orderseqlem 30993 soseq 30995 elno 31043 filnetlem4 31546 bj-finsumval0 32324 poimirlem25 32604 poimirlem28 32607 volsupnfl 32624 mbfresfi 32626 upixp 32694 sdclem2 32708 sdclem1 32709 fdc 32711 ismgmOLD 32819 elghomlem2OLD 32855 istendo 35066 ismrc 36282 fmuldfeqlem1 38649 fmuldfeq 38650 dvnprodlem1 38836 stoweidlem15 38908 stoweidlem16 38909 stoweidlem17 38910 stoweidlem19 38912 stoweidlem20 38913 stoweidlem21 38914 stoweidlem22 38915 stoweidlem23 38916 stoweidlem27 38920 stoweidlem31 38924 stoweidlem32 38925 stoweidlem42 38935 stoweidlem48 38941 stoweidlem51 38944 stoweidlem59 38952 isomenndlem 39420 griedg0prc 40488 lincdifsn 42007 |
Copyright terms: Public domain | W3C validator |