![]() |
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 5300 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) | |
2 | 1 | anbi1d 465 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶) ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶))) |
3 | df-f 5215 | . 2 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)) | |
4 | df-f 5215 | . 2 ⊢ (𝐹:𝐵⟶𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶)) | |
5 | 2, 3, 4 | 3bitr4g 223 | 1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1353 ⊆ wss 3129 ran crn 4623 Fn wfn 5206 ⟶wf 5207 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-4 1510 ax-17 1526 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 df-fn 5214 df-f 5215 |
This theorem is referenced by: feq23 5346 feq2d 5348 feq2i 5354 f00 5402 f0dom0 5404 f1eq2 5412 fressnfv 5698 tfrcllemsucfn 6347 tfrcllemsucaccv 6348 tfrcllembxssdm 6350 tfrcllembfn 6351 tfrcllemaccex 6355 tfrcllemres 6356 tfrcldm 6357 tfrcl 6358 mapvalg 6651 map0g 6681 ac6sfi 6891 isomni 7127 ismkv 7144 iswomni 7156 |
Copyright terms: Public domain | W3C validator |