| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > fneq2d | Structured version Visualization version GIF version | ||
| Description: Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.) |
| Ref | Expression |
|---|---|
| fneq2d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
| Ref | Expression |
|---|---|
| fneq2d | ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fneq2d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 2 | fneq2 6617 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) | |
| 3 | 1, 2 | syl 18 | 1 ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 209 = wceq 1563 Fn wfn 6520 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-9 2155 ax-ext 2737 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-ex 1803 df-cleq 2757 df-fn 6528 |
| This theorem is referenced by: fneq12d 6620 fncofn 6642 fnco 6643 fnprb 7196 fntpb 7197 fnpr2g 7198 undifixp 8920 brwdom2 9523 brttrcl2 9671 ssttrcl 9672 ttrcltr 9673 ttrclss 9677 ttrclselem2 9683 dfac3 10093 ac7g 10446 ccatlid 14614 ccatrid 14615 ccatass 14616 ccatswrd 14696 swrdccat2 14697 ccatpfx 14728 swrdswrd 14732 swrdccatin2 14756 pfxccatin12 14760 revccat 14793 revrev 14794 repsdf2 14805 0csh0 14820 cshco 14863 wrd2pr2op 14970 wrd3tpop 14975 ofccat 14996 seqshft 15112 invf 17815 sscfn1 17864 sscfn2 17865 isssc 17867 fuchom 18011 estrchomfeqhom 18182 mulgfval 19126 mulgfvalALT 19127 srhmsubc 20756 frlmsslss2 21885 subrgascl 22177 selvvvval 22253 m1detdiag 22715 ptval 23688 xpsdsfn2 24496 fresf1o 32888 psgndmfi 33331 cycpmconjslem1 33387 cycpmconjslem2 33388 ply1annidllem 34008 pl1cn 34262 signsvtn0 34874 signstres 34879 bnj927 35075 fineqvac 35424 revpfxsfxrev 35478 ixpeq12dv 36589 cbvixpdavw 36651 cbvixpdavw2 36667 poimirlem1 38132 poimirlem2 38133 poimirlem3 38134 poimirlem4 38135 poimirlem6 38137 poimirlem7 38138 poimirlem11 38142 poimirlem12 38143 poimirlem16 38147 poimirlem17 38148 poimirlem19 38150 poimirlem20 38151 dibfnN 41792 dihintcl 41980 frlmvscadiccat 43140 ofoafg 43943 uzmptshftfval 44920 srhmsubcALTV 48945 tposideq 49517 nelsubc3lem 49699 0funcg2 49713 fucofulem2 49940 termcfuncval 50161 termcnatval 50164 0fucterm 50172 cnelsubclem 50232 |
| Copyright terms: Public domain | W3C validator |