Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > feq2d | GIF version |
Description: Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.) |
Ref | Expression |
---|---|
feq2d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
feq2d | ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | feq2d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | feq2 5331 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 = wceq 1348 ⟶wf 5194 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1440 ax-gen 1442 ax-4 1503 ax-17 1519 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-cleq 2163 df-fn 5201 df-f 5202 |
This theorem is referenced by: feq12d 5337 ffdm 5368 fsng 5669 issmo2 6268 qliftf 6598 elpm2r 6644 casef 7065 fseq1p1m1 10050 fseq1m1p1 10051 seqf 10417 seqf2 10420 intopsn 12621 lmtopcnp 13044 ellimc3apf 13423 dvidlemap 13454 dviaddf 13463 dvimulf 13464 dvcjbr 13466 dvcj 13467 dvrecap 13471 dvmptclx 13474 |
Copyright terms: Public domain | W3C validator |