![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fneq1i | Structured version Visualization version Unicode version |
Description: Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.) |
Ref | Expression |
---|---|
fneq1i.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
fneq1i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fneq1i.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | fneq1 5686 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-rab 2758 df-v 3059 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-sn 3981 df-pr 3983 df-op 3987 df-br 4417 df-opab 4476 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-fun 5603 df-fn 5604 |
This theorem is referenced by: fnunsn 5705 mptfnf 5721 fnopabg 5723 f1oun 5856 f1oi 5873 f1osn 5875 ovid 6440 curry1 6915 curry2 6918 wfrlem5 7066 wfrlem13 7074 tfrlem10 7131 tfr1 7141 seqomlem2 7194 seqomlem3 7195 seqomlem4 7196 fnseqom 7198 unblem4 7852 r1fnon 8264 alephfnon 8522 alephfplem4 8564 alephfp 8565 cfsmolem 8726 infpssrlem3 8761 compssiso 8830 hsmexlem5 8886 axdclem2 8976 wunex2 9189 wuncval2 9198 om2uzrani 12198 om2uzf1oi 12199 uzrdglem 12203 uzrdgfni 12204 uzrdg0i 12205 hashkf 12549 dmaf 15993 cdaf 15994 prdsinvlem 16843 srg1zr 17811 pws1 17893 frlmphl 19388 ovolunlem1 22499 0plef 22679 0pledm 22680 itg1ge0 22693 itg1addlem4 22706 mbfi1fseqlem5 22726 itg2addlem 22765 qaa 23328 2trllemD 25336 eupap1 25753 ghgrpOLD 26145 0vfval 26274 xrge0pluscn 28795 bnj927 29629 bnj535 29750 frrlem5 30567 fullfunfnv 30762 neibastop2lem 31065 fourierdlem42 38050 fourierdlem42OLD 38051 rngcrescrhm 40360 rngcrescrhmALTV 40379 |
Copyright terms: Public domain | W3C validator |