![]() |
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 5364 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 = wceq 1364 ⟶wf 5227 |
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 1458 ax-gen 1460 ax-4 1521 ax-17 1537 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-cleq 2182 df-fn 5234 df-f 5235 |
This theorem is referenced by: feq12d 5370 ffdm 5401 fsng 5705 issmo2 6308 qliftf 6638 elpm2r 6684 casef 7105 fseq1p1m1 10112 fseq1m1p1 10113 seqf 10479 seqf2 10482 intopsn 12809 resmhm 12905 isghm 13143 resghm 13160 lmtopcnp 14147 ellimc3apf 14526 dvidlemap 14557 dviaddf 14566 dvimulf 14567 dvcjbr 14569 dvcj 14570 dvrecap 14574 dvmptclx 14577 |
Copyright terms: Public domain | W3C validator |