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 6437 | . 2 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 Fn wfn 6343 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-br 5058 df-opab 5120 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-fun 6350 df-fn 6351 |
This theorem is referenced by: fneq12d 6441 f1o00 6642 f1oprswap 6651 f1ompt 6867 fmpt2d 6879 f1ocnvd 7385 offn 7409 offval2f 7410 offval2 7415 ofrfval2 7416 caofinvl 7425 fsplitfpar 7803 omxpenlem 8606 itunifn 9827 konigthlem 9978 seqof 13415 swrdlen 13997 mptfzshft 15121 fprodrev 15319 prdsdsfn 16726 imasdsfn 16775 cidfn 16938 comffn 16963 isoval 17023 invf1o 17027 isofn 17033 brssc 17072 cofucl 17146 estrchomfn 17373 funcestrcsetclem4 17381 funcsetcestrclem4 17396 1stfcl 17435 2ndfcl 17436 prfcl 17441 evlfcl 17460 curf1cl 17466 curfcl 17470 hofcl 17497 yonedainv 17519 grpinvf1o 18107 pmtrrn 18514 pmtrfrn 18515 srngf1o 19554 ofco2 20988 mat1dimscm 21012 neif 21636 fmf 22481 fncpn 24457 mdeg0 24591 tglnfn 26260 grpoinvf 28236 kbass2 29821 fnresin 30299 f1o3d 30300 suppovss 30354 f1od2 30383 frlmdim 30908 pstmxmet 31036 prodindf 31181 ofcfn 31258 ofcfval2 31262 signstlen 31736 bnj941 31943 satfn 32499 msubrn 32673 poimirlem4 34777 cnambfre 34821 sdclem2 34898 diafn 38050 dibfna 38170 dicfnN 38199 dihf11lem 38282 mapd1o 38664 hdmapfnN 38845 hgmapfnN 38904 hbtlem7 39603 fsovf1od 40240 ntrrn 40350 ntrf 40351 dssmapntrcls 40356 addrfn 40681 subrfn 40682 mulvfn 40683 fsumsermpt 41736 hoidmvlelem3 42756 smflimsuplem7 42977 smndex1n0mnd 44012 rnghmresfn 44162 rhmresfn 44208 funcringcsetcALTV2lem4 44238 funcringcsetclem4ALTV 44261 rhmsubclem1 44285 rhmsubcALTVlem1 44303 |
Copyright terms: Public domain | W3C validator |