Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fneq1d | Structured version Visualization version GIF version |
Description: Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.) |
Ref | Expression |
---|---|
fneq1d.1 | ⊢ (𝜑 → 𝐹 = 𝐺) |
Ref | Expression |
---|---|
fneq1d | ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fneq1d.1 | . 2 ⊢ (𝜑 → 𝐹 = 𝐺) | |
2 | fneq1 6439 | . 2 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 = wceq 1533 Fn wfn 6345 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3497 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4562 df-pr 4564 df-op 4568 df-br 5060 df-opab 5122 df-rel 5557 df-cnv 5558 df-co 5559 df-dm 5560 df-fun 6352 df-fn 6353 |
This theorem is referenced by: fneq12d 6443 f1o00 6644 f1oprswap 6653 f1ompt 6870 fmpt2d 6882 f1ocnvd 7390 offn 7414 offval2f 7415 offval2 7420 ofrfval2 7421 caofinvl 7430 fsplitfpar 7808 omxpenlem 8612 itunifn 9833 konigthlem 9984 seqof 13421 swrdlen 14003 mptfzshft 15127 fprodrev 15325 prdsdsfn 16732 imasdsfn 16781 cidfn 16944 comffn 16969 isoval 17029 invf1o 17033 isofn 17039 brssc 17078 cofucl 17152 estrchomfn 17379 funcestrcsetclem4 17387 funcsetcestrclem4 17402 1stfcl 17441 2ndfcl 17442 prfcl 17447 evlfcl 17466 curf1cl 17472 curfcl 17476 hofcl 17503 yonedainv 17525 smndex1n0mnd 18071 grpinvf1o 18163 pmtrrn 18579 pmtrfrn 18580 srngf1o 19619 ofco2 21054 mat1dimscm 21078 neif 21702 fmf 22547 fncpn 24524 mdeg0 24658 tglnfn 26327 grpoinvf 28303 kbass2 29888 fnresin 30365 f1o3d 30366 suppovss 30420 f1od2 30451 frlmdim 31004 pstmxmet 31132 prodindf 31277 ofcfn 31354 ofcfval2 31358 signstlen 31832 bnj941 32039 satfn 32597 msubrn 32771 poimirlem4 34890 cnambfre 34934 sdclem2 35011 diafn 38164 dibfna 38284 dicfnN 38313 dihf11lem 38396 mapd1o 38778 hdmapfnN 38959 hgmapfnN 39018 hbtlem7 39718 fsovf1od 40355 ntrrn 40465 ntrf 40466 dssmapntrcls 40471 addrfn 40797 subrfn 40798 mulvfn 40799 fsumsermpt 41852 hoidmvlelem3 42872 smflimsuplem7 43093 rnghmresfn 44227 rhmresfn 44273 funcringcsetcALTV2lem4 44303 funcringcsetclem4ALTV 44326 rhmsubclem1 44350 rhmsubcALTVlem1 44368 |
Copyright terms: Public domain | W3C validator |