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 5894 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 = wceq 1475 Fn wfn 5799 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-an 385 df-cleq 2603 df-fn 5807 |
This theorem is referenced by: fneq12d 5897 fnprb 6377 fntpb 6378 fnpr2g 6379 undifixp 7830 brwdom2 8361 dfac3 8827 ac7g 9179 ccatlid 13222 ccatrid 13223 ccatass 13224 ccatswrd 13308 swrdccat2 13310 swrdswrd 13312 swrdccatin2 13338 swrdccatin12 13342 revccat 13366 revrev 13367 repsdf2 13376 0csh0 13390 cshco 13433 wrd2pr2op 13535 wrd3tpop 13539 ofccat 13556 seqshft 13673 invf 16251 sscfn1 16300 sscfn2 16301 isssc 16303 fuchom 16444 estrchomfeqhom 16599 mulgfval 17365 symgplusg 17632 subrgascl 19319 frlmsslss2 19933 m1detdiag 20222 ptval 21183 xpsdsfn2 21993 fresf1o 28815 psgndmfi 29177 pl1cn 29329 signsvtn0 29973 signstres 29978 bnj927 30093 poimirlem1 32580 poimirlem2 32581 poimirlem3 32582 poimirlem4 32583 poimirlem6 32585 poimirlem7 32586 poimirlem11 32590 poimirlem12 32591 poimirlem16 32595 poimirlem17 32596 poimirlem19 32598 poimirlem20 32599 dibfnN 35463 dihintcl 35651 uzmptshftfval 37567 ccatpfx 40272 pfxccatin12 40288 srhmsubc 41868 srhmsubcALTV 41887 |
Copyright terms: Public domain | W3C validator |