![]() |
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 6227 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1601 Fn wfn 6132 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1824 df-cleq 2770 df-fn 6140 |
This theorem is referenced by: fneq12d 6230 fnprb 6746 fntpb 6747 fnpr2g 6748 undifixp 8232 brwdom2 8769 dfac3 9279 ac7g 9633 ccatlid 13680 ccatrid 13681 ccatass 13682 ccatswrd 13780 swrdccat2 13782 ccatpfx 13814 swrdswrd 13818 swrdccatin2 13860 pfxccatin12 13865 swrdccatin12OLD 13866 revccat 13916 revrev 13917 repsdf2 13928 0csh0 13947 0csh0OLD 13948 cshco 13991 wrd2pr2op 14098 wrd3tpop 14103 ofccat 14121 seqshft 14236 invf 16817 sscfn1 16866 sscfn2 16867 isssc 16869 fuchom 17010 estrchomfeqhom 17165 mulgfval 17933 symgplusg 18196 subrgascl 19898 frlmsslss2 20522 m1detdiag 20812 ptval 21786 xpsdsfn2 22595 fresf1o 30002 psgndmfi 30448 pl1cn 30603 signsvtn0 31251 signsvtn0OLD 31252 signstres 31257 bnj927 31442 poimirlem1 34041 poimirlem2 34042 poimirlem3 34043 poimirlem4 34044 poimirlem6 34046 poimirlem7 34047 poimirlem11 34051 poimirlem12 34052 poimirlem16 34056 poimirlem17 34057 poimirlem19 34059 poimirlem20 34060 dibfnN 37315 dihintcl 37503 uzmptshftfval 39511 srhmsubc 43101 srhmsubcALTV 43119 |
Copyright terms: Public domain | W3C validator |