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 5980 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) | |
2 | 1 | anbi1d 741 | . 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-ext 2602 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-cleq 2615 df-fn 5891 df-f 5892 |
This theorem is referenced by: feq23 6029 feq2d 6031 feq2i 6037 f00 6087 f0dom0 6089 f1eq2 6097 fressnfv 6427 mapvalg 7867 map0g 7897 ac6sfi 8204 cofsmo 9091 axcc4dom 9263 ac6sg 9310 isghm 17660 pjdm2 20055 cmpcovf 21194 ulmval 24134 measval 30261 isrnmeas 30263 poseq 31750 soseq 31751 elno2 31807 noreson 31813 bj-finsumval0 33147 mbfresfi 33456 stoweidlem62 40279 hoidmvval0b 40804 vonioo 40896 vonicc 40899 |
Copyright terms: Public domain | W3C validator |