![]() |
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 6641 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1540 Fn wfn 6538 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1781 df-cleq 2723 df-fn 6546 |
This theorem is referenced by: fneq12d 6644 fncofn 6666 fnco 6667 fnprb 7212 fntpb 7213 fnpr2g 7214 undifixp 8934 brwdom2 9574 brttrcl2 9715 ssttrcl 9716 ttrcltr 9717 ttrclss 9721 ttrclselem2 9727 dfac3 10122 ac7g 10475 ccatlid 14543 ccatrid 14544 ccatass 14545 ccatswrd 14625 swrdccat2 14626 ccatpfx 14658 swrdswrd 14662 swrdccatin2 14686 pfxccatin12 14690 revccat 14723 revrev 14724 repsdf2 14735 0csh0 14750 cshco 14794 wrd2pr2op 14901 wrd3tpop 14906 ofccat 14923 seqshft 15039 invf 17722 sscfn1 17771 sscfn2 17772 isssc 17774 fuchom 17923 fuchomOLD 17924 estrchomfeqhom 18097 mulgfval 18995 mulgfvalALT 18996 srhmsubc 20572 frlmsslss2 21641 subrgascl 21939 m1detdiag 22420 ptval 23395 xpsdsfn2 24205 fresf1o 32290 psgndmfi 32695 cycpmconjslem1 32751 cycpmconjslem2 32752 ply1annidllem 33219 pl1cn 33401 signsvtn0 34047 signstres 34052 bnj927 34246 fineqvac 34563 revpfxsfxrev 34572 poimirlem1 36956 poimirlem2 36957 poimirlem3 36958 poimirlem4 36959 poimirlem6 36961 poimirlem7 36962 poimirlem11 36966 poimirlem12 36967 poimirlem16 36971 poimirlem17 36972 poimirlem19 36974 poimirlem20 36975 dibfnN 40494 dihintcl 40682 frlmvscadiccat 41550 selvvvval 41623 ofoafg 42570 uzmptshftfval 43571 srhmsubcALTV 47165 |
Copyright terms: Public domain | W3C validator |