![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > feq3 | Structured version Visualization version GIF version |
Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
feq3 | ⊢ (𝐴 = 𝐵 → (𝐹:𝐶⟶𝐴 ↔ 𝐹:𝐶⟶𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseq2 3971 | . . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 ⊆ 𝐴 ↔ ran 𝐹 ⊆ 𝐵)) | |
2 | 1 | anbi2d 630 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐵))) |
3 | df-f 6501 | . 2 ⊢ (𝐹:𝐶⟶𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐴)) | |
4 | df-f 6501 | . 2 ⊢ (𝐹:𝐶⟶𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐵)) | |
5 | 2, 3, 4 | 3bitr4g 314 | 1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶⟶𝐴 ↔ 𝐹:𝐶⟶𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ⊆ wss 3911 ran crn 5635 Fn wfn 6492 ⟶wf 6493 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3446 df-in 3918 df-ss 3928 df-f 6501 |
This theorem is referenced by: feq23 6653 feq3d 6656 fun2 6706 fconstg 6730 f1eq3 6736 mapvalg 8778 mapsnd 8827 cantnff 9615 axdc4uz 13895 supcvg 15746 lmff 22668 txcn 22993 lmmbr 24638 iscmet3 24673 dvcnvrelem2 25398 itgsubstlem 25428 umgrislfupgr 28116 usgrislfuspgr 28177 wlkv0 28641 isgrpo 29481 vciOLD 29545 isvclem 29561 nmop0h 30975 sitgaddlemb 33005 sitmcl 33008 cvmliftlem15 33949 mtyf 34203 matunitlindflem1 36120 sdclem1 36248 k0004lem1 42507 stoweidlem57 44384 f1ocof1ob 45399 isomushgr 46104 mof02 46991 mofsn2 46997 mofeu 47000 fdomne0 47002 f002 47006 fullthinc 47152 |
Copyright terms: Public domain | W3C validator |