![]() |
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 6637 | . 2 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1542 Fn wfn 6535 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-br 5148 df-opab 5210 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-fun 6542 df-fn 6543 |
This theorem is referenced by: fneq12d 6641 f1o00 6865 f1oprswap 6874 f1ompt 7106 fmpt2d 7118 f1ocnvd 7652 offn 7678 offval2f 7680 offval2 7685 ofrfval2 7686 caofinvl 7695 fsplitfpar 8099 omxpenlem 9069 itunifn 10408 konigthlem 10559 seqof 14021 swrdlen 14593 mptfzshft 15720 prdsdsfn 17407 imasdsfn 17456 cidfn 17619 comffn 17645 isoval 17708 invf1o 17712 isofn 17718 brssc 17757 cofucl 17834 estrchomfn 18082 funcestrcsetclem4 18091 funcsetcestrclem4 18106 1stfcl 18145 2ndfcl 18146 prfcl 18151 evlfcl 18171 curf1cl 18177 curfcl 18181 hofcl 18208 yonedainv 18230 smndex1n0mnd 18789 grpinvf1o 18889 pmtrrn 19318 pmtrfrn 19319 srngf1o 20450 ofco2 21935 mat1dimscm 21959 neif 22586 fmf 23431 fncpn 25432 mdeg0 25570 tglnfn 27778 grpoinvf 29763 kbass2 31348 fnresin 31828 f1o3d 31829 suppovss 31884 f1od2 31924 ghmquskerco 32492 frlmdim 32641 pstmxmet 32815 prodindf 32959 ofcfn 33036 ofcfval2 33040 signstlen 33516 bnj941 33721 satfn 34284 msubrn 34458 poimirlem4 36430 cnambfre 36474 sdclem2 36548 diafn 39843 dibfna 39963 dicfnN 39992 dihf11lem 40075 mapd1o 40457 hdmapfnN 40638 hgmapfnN 40697 aks4d1p1p5 40878 hbtlem7 41800 fsovf1od 42700 ntrrn 42806 ntrf 42807 dssmapntrcls 42812 addrfn 43164 subrfn 43165 mulvfn 43166 fsumsermpt 44230 hoidmvlelem3 45248 smflimsuplem7 45477 rnghmresfn 46763 rhmresfn 46809 funcringcsetcALTV2lem4 46839 funcringcsetclem4ALTV 46862 rhmsubclem1 46886 rhmsubcALTVlem1 46904 ackvalsucsucval 47276 |
Copyright terms: Public domain | W3C validator |