| 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 14612 ccatrid 14613 ccatass 14614 ccatswrd 14694 swrdccat2 14695 ccatpfx 14726 swrdswrd 14730 swrdccatin2 14754 pfxccatin12 14758 revccat 14791 revrev 14792 repsdf2 14803 0csh0 14818 cshco 14861 wrd2pr2op 14968 wrd3tpop 14973 ofccat 14994 seqshft 15110 invf 17813 sscfn1 17862 sscfn2 17863 isssc 17865 fuchom 18009 estrchomfeqhom 18180 mulgfval 19123 mulgfvalALT 19124 srhmsubc 20753 frlmsslss2 21882 subrgascl 22174 selvvvval 22250 m1detdiag 22711 ptval 23684 xpsdsfn2 24492 fresf1o 32884 psgndmfi 33326 cycpmconjslem1 33382 cycpmconjslem2 33383 ply1annidllem 34003 pl1cn 34257 signsvtn0 34869 signstres 34874 bnj927 35070 fineqvac 35419 revpfxsfxrev 35473 ixpeq12dv 36584 cbvixpdavw 36646 cbvixpdavw2 36662 poimirlem1 38127 poimirlem2 38128 poimirlem3 38129 poimirlem4 38130 poimirlem6 38132 poimirlem7 38133 poimirlem11 38137 poimirlem12 38138 poimirlem16 38142 poimirlem17 38143 poimirlem19 38145 poimirlem20 38146 dibfnN 41787 dihintcl 41975 frlmvscadiccat 43135 ofoafg 43938 uzmptshftfval 44915 srhmsubcALTV 48946 tposideq 49518 nelsubc3lem 49700 0funcg2 49714 fucofulem2 49941 termcfuncval 50162 termcnatval 50165 0fucterm 50173 cnelsubclem 50233 |
| Copyright terms: Public domain | W3C validator |