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 5315 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 = wceq 1342 ⟶wf 5178 |
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 1434 ax-gen 1436 ax-4 1497 ax-17 1513 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-cleq 2157 df-fn 5185 df-f 5186 |
This theorem is referenced by: feq12d 5321 ffdm 5352 fsng 5652 issmo2 6248 qliftf 6577 elpm2r 6623 casef 7044 fseq1p1m1 10019 fseq1m1p1 10020 seqf 10386 seqf2 10389 lmtopcnp 12797 ellimc3apf 13176 dvidlemap 13207 dviaddf 13216 dvimulf 13217 dvcjbr 13219 dvcj 13220 dvrecap 13224 dvmptclx 13227 |
Copyright terms: Public domain | W3C validator |