| 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 4010 | . . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 ⊆ 𝐴 ↔ ran 𝐹 ⊆ 𝐵)) | |
| 2 | 1 | anbi2d 630 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐵))) |
| 3 | df-f 6565 | . 2 ⊢ (𝐹:𝐶⟶𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐴)) | |
| 4 | df-f 6565 | . 2 ⊢ (𝐹:𝐶⟶𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐵)) | |
| 5 | 2, 3, 4 | 3bitr4g 314 | 1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶⟶𝐴 ↔ 𝐹:𝐶⟶𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ⊆ wss 3951 ran crn 5686 Fn wfn 6556 ⟶wf 6557 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-ss 3968 df-f 6565 |
| This theorem is referenced by: feq23 6719 feq3d 6723 fun2 6771 fconstg 6795 f1eq3 6801 mapvalg 8876 mapsnd 8926 cantnff 9714 axdc4uz 14025 supcvg 15892 lmff 23309 txcn 23634 lmmbr 25292 iscmet3 25327 dvcnvrelem2 26057 itgsubstlem 26089 umgrislfupgr 29140 uspgriedgedg 29193 usgrislfuspgr 29204 wlkv0 29669 isgrpo 30516 vciOLD 30580 isvclem 30596 nmop0h 32010 sitgaddlemb 34350 sitmcl 34353 cvmliftlem15 35303 mtyf 35557 matunitlindflem1 37623 sdclem1 37750 k0004lem1 44160 relpeq5 44969 stoweidlem57 46072 f1ocof1ob 47093 isuspgrim0lem 47871 gricushgr 47886 uspgrlimlem4 47958 mof02 48748 mofsn2 48754 mofeu 48757 fdomne0 48759 f002 48763 fullthinc 49099 functermc 49140 |
| Copyright terms: Public domain | W3C validator |