![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > feq2 | GIF version |
Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
feq2 | ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fneq2 5056 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) | |
2 | 1 | anbi1d 453 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶) ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶))) |
3 | df-f 4973 | . 2 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)) | |
4 | df-f 4973 | . 2 ⊢ (𝐹:𝐵⟶𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶)) | |
5 | 2, 3, 4 | 3bitr4g 221 | 1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ↔ wb 103 = wceq 1285 ⊆ wss 2984 ran crn 4402 Fn wfn 4964 ⟶wf 4965 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1377 ax-gen 1379 ax-4 1441 ax-17 1460 ax-ext 2065 |
This theorem depends on definitions: df-bi 115 df-cleq 2076 df-fn 4972 df-f 4973 |
This theorem is referenced by: feq23 5101 feq2d 5103 feq2i 5108 f00 5150 f0dom0 5152 f1eq2 5160 fressnfv 5426 tfrcllemsucfn 6050 tfrcllemsucaccv 6051 tfrcllembxssdm 6053 tfrcllembfn 6054 tfrcllemaccex 6058 tfrcllemres 6059 tfrcldm 6060 tfrcl 6061 mapvalg 6345 map0g 6375 ac6sfi 6544 isomni 6697 |
Copyright terms: Public domain | W3C validator |