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 3627 | . . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 ⊆ 𝐴 ↔ ran 𝐹 ⊆ 𝐵)) | |
2 | 1 | anbi2d 740 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐵))) |
3 | df-f 5892 | . 2 ⊢ (𝐹:𝐶⟶𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐴)) | |
4 | df-f 5892 | . 2 ⊢ (𝐹:𝐶⟶𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐵)) | |
5 | 2, 3, 4 | 3bitr4g 303 | 1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶⟶𝐴 ↔ 𝐹:𝐶⟶𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1483 ⊆ wss 3574 ran crn 5115 Fn wfn 5883 ⟶wf 5884 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-in 3581 df-ss 3588 df-f 5892 |
This theorem is referenced by: feq23 6029 feq3d 6032 fun2 6067 fconstg 6092 f1eq3 6098 mapvalg 7867 mapsn 7899 cantnff 8571 axdc4uz 12783 supcvg 14588 lmff 21105 txcn 21429 lmmbr 23056 iscmet3 23091 dvcnvrelem2 23781 itgsubstlem 23811 umgrislfupgr 26018 usgrislfuspgr 26079 wlkv0 26547 isgrpo 27351 vciOLD 27416 isvclem 27432 nmop0h 28850 sitgaddlemb 30410 sitmcl 30413 cvmliftlem15 31280 mtyf 31449 matunitlindflem1 33405 sdclem1 33539 k0004lem1 38445 mapsnd 39388 stoweidlem57 40274 |
Copyright terms: Public domain | W3C validator |