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 6430 | . . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) | |
2 | rneq 5780 | . . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺) | |
3 | 2 | sseq1d 3909 | . . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵)) |
4 | 1, 3 | anbi12d 634 | . 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))) |
5 | df-f 6344 | . 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
6 | df-f 6344 | . 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)) | |
7 | 4, 5, 6 | 3bitr4g 317 | 1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1542 ⊆ wss 3844 ran crn 5527 Fn wfn 6335 ⟶wf 6336 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2711 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-v 3401 df-un 3849 df-in 3851 df-ss 3861 df-sn 4518 df-pr 4520 df-op 4524 df-br 5032 df-opab 5094 df-rel 5533 df-cnv 5534 df-co 5535 df-dm 5536 df-rn 5537 df-fun 6342 df-fn 6343 df-f 6344 |
This theorem is referenced by: feq1d 6490 feq1i 6496 elimf 6504 f00 6561 f0bi 6562 f0dom0 6563 fconstg 6566 f1eq1 6570 fprb 6969 fconst2g 6978 fsnex 7053 elmapg 8453 mapfset 8463 fsetsspwxp 8466 fsetfcdm 8473 fsetfocdm 8474 fsetprcnex 8475 ac6sfi 8839 updjud 9439 ac5num 9539 acni2 9549 cofsmo 9772 cfsmolem 9773 cfcoflem 9775 coftr 9776 alephsing 9779 axdc2lem 9951 axdc3lem2 9954 axdc3lem3 9955 axdc3 9957 axdc4lem 9958 ac6num 9982 inar1 10278 axdc4uzlem 13445 seqf1olem2 13505 seqf1o 13506 iswrd 13960 cshf1 14264 wrdlen2i 14396 ramub2 16453 ramcl 16468 isacs2 17030 isacs1i 17034 mreacs 17035 mgmb1mgm1 17984 elefmndbas2 18158 isgrpinv 18277 isghm 18479 islindf 20631 mat1dimelbas 21225 1stcfb 22199 upxp 22377 txcn 22380 isi1f 24429 mbfi1fseqlem6 24476 mbfi1flimlem 24478 itg2addlem 24514 plyf 24950 griedg0prc 27209 isgrpo 28435 vciOLD 28499 isvclem 28515 isnvlem 28548 ajmoi 28796 ajval 28799 hlimi 29126 chlimi 29172 chcompl 29180 adjmo 29770 adjeu 29827 adjval 29828 adj1 29871 adjeq 29873 cnlnssadj 30018 pjinvari 30129 padct 30632 locfinref 31366 isrnmeas 31741 orderseqlem 33417 soseq 33419 elno 33495 filnetlem4 34216 bj-finsumval0 35100 poimirlem25 35448 poimirlem28 35451 volsupnfl 35468 mbfresfi 35469 upixp 35533 sdclem2 35546 sdclem1 35547 fdc 35549 ismgmOLD 35654 elghomlem2OLD 35690 istendo 38420 sticksstones1 39731 sticksstones2 39732 sticksstones3 39733 sticksstones8 39738 ismrc 40118 fmuldfeqlem1 42688 fmuldfeq 42689 dvnprodlem1 43052 stoweidlem15 43121 stoweidlem16 43122 stoweidlem17 43123 stoweidlem19 43125 stoweidlem20 43126 stoweidlem21 43127 stoweidlem22 43128 stoweidlem23 43129 stoweidlem27 43133 stoweidlem31 43137 stoweidlem32 43138 stoweidlem42 43148 stoweidlem48 43154 stoweidlem51 43157 stoweidlem59 43165 isomenndlem 43633 smfpimcclem 43902 fsetsniunop 44105 cfsetsnfsetf 44114 cfsetsnfsetf1 44115 cfsetsnfsetfo 44116 lincdifsn 45329 0aryfvalel 45544 mof0ALT 45727 mofsn 45731 |
Copyright terms: Public domain | W3C validator |