![]() |
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 5170 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) | |
2 | 1 | anbi1d 458 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶) ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶))) |
3 | df-f 5085 | . 2 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)) | |
4 | df-f 5085 | . 2 ⊢ (𝐹:𝐵⟶𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶)) | |
5 | 2, 3, 4 | 3bitr4g 222 | 1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 = wceq 1314 ⊆ wss 3037 ran crn 4500 Fn wfn 5076 ⟶wf 5077 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1406 ax-gen 1408 ax-4 1470 ax-17 1489 ax-ext 2097 |
This theorem depends on definitions: df-bi 116 df-cleq 2108 df-fn 5084 df-f 5085 |
This theorem is referenced by: feq23 5216 feq2d 5218 feq2i 5224 f00 5272 f0dom0 5274 f1eq2 5282 fressnfv 5561 tfrcllemsucfn 6204 tfrcllemsucaccv 6205 tfrcllembxssdm 6207 tfrcllembfn 6208 tfrcllemaccex 6212 tfrcllemres 6213 tfrcldm 6214 tfrcl 6215 mapvalg 6506 map0g 6536 ac6sfi 6745 isomni 6958 ismkv 6977 |
Copyright terms: Public domain | W3C validator |