Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > feq2 | Structured version Visualization version GIF version |
Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
feq2 | ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fneq2 5894 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) | |
2 | 1 | anbi1d 737 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶) ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶))) |
3 | df-f 5808 | . 2 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)) | |
4 | df-f 5808 | . 2 ⊢ (𝐹:𝐵⟶𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶)) | |
5 | 2, 3, 4 | 3bitr4g 302 | 1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ⊆ wss 3540 ran crn 5039 Fn wfn 5799 ⟶wf 5800 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-an 385 df-cleq 2603 df-fn 5807 df-f 5808 |
This theorem is referenced by: feq23 5942 feq2d 5944 feq2i 5950 f00 6000 f0dom0 6002 f1eq2 6010 fressnfv 6332 mapvalg 7754 map0g 7783 ac6sfi 8089 cofsmo 8974 axcc4dom 9146 ac6sg 9193 isghm 17483 pjdm2 19874 cmpcovf 21004 ulmval 23938 measval 29588 isrnmeas 29590 poseq 30994 soseq 30995 elno2 31051 noreson 31057 noxpsgn 31062 nodenselem6 31085 bj-finsumval0 32324 mbfresfi 32626 stoweidlem62 38955 hoidmvval0b 39480 vonioo 39573 vonicc 39576 |
Copyright terms: Public domain | W3C validator |