![]() |
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 3660 | . . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 ⊆ 𝐴 ↔ ran 𝐹 ⊆ 𝐵)) | |
2 | 1 | anbi2d 740 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐵))) |
3 | df-f 5930 | . 2 ⊢ (𝐹:𝐶⟶𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐴)) | |
4 | df-f 5930 | . 2 ⊢ (𝐹:𝐶⟶𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐵)) | |
5 | 2, 3, 4 | 3bitr4g 303 | 1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶⟶𝐴 ↔ 𝐹:𝐶⟶𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1523 ⊆ wss 3607 ran crn 5144 Fn wfn 5921 ⟶wf 5922 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-in 3614 df-ss 3621 df-f 5930 |
This theorem is referenced by: feq23 6067 feq3d 6070 fun2 6105 fconstg 6130 f1eq3 6136 mapvalg 7909 mapsn 7941 cantnff 8609 axdc4uz 12823 supcvg 14632 lmff 21153 txcn 21477 lmmbr 23102 iscmet3 23137 dvcnvrelem2 23826 itgsubstlem 23856 umgrislfupgr 26063 usgrislfuspgr 26124 wlkv0 26603 isgrpo 27479 vciOLD 27544 isvclem 27560 nmop0h 28978 sitgaddlemb 30538 sitmcl 30541 cvmliftlem15 31406 mtyf 31575 matunitlindflem1 33535 sdclem1 33669 k0004lem1 38762 mapsnd 39702 stoweidlem57 40592 |
Copyright terms: Public domain | W3C validator |