![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfcvd | Structured version Visualization version Unicode version |
Description: If ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfcvd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2594 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | a1i 11 |
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 1671 ax-5 1760 |
This theorem depends on definitions: df-bi 189 df-nf 1670 df-nfc 2583 |
This theorem is referenced by: nfeld 2602 ralcom2 2957 vtoclgft 3098 vtocld 3100 sbcralt 3342 sbcrext 3343 csbied 3392 csbie2t 3394 sbcco3g 3790 csbco3g 3791 dfnfc2 4219 eusvnfb 4602 eusv2i 4603 dfid3 4753 nfiotad 5552 iota2d 5574 iota2 5575 fmptcof 6062 riota5f 6281 riota5 6282 oprabid 6322 opiota 6857 fmpt2co 6884 axrepndlem1 9022 axrepndlem2 9023 axunnd 9026 axpowndlem2 9028 axpowndlem3 9029 axpowndlem4 9030 axpownd 9031 axregndlem2 9033 axinfndlem1 9035 axinfnd 9036 axacndlem4 9040 axacndlem5 9041 axacnd 9042 nfnegd 9875 sumsn 13819 prodsn 14028 fprodeq0g 14060 bpolylem 14113 pcmpt 14849 chfacfpmmulfsupp 19899 elmptrab 20854 dvfsumrlim3 22997 itgsubstlem 23012 itgsubst 23013 ifeqeqx 28170 disjunsn 28216 unirep 32051 riotasv2d 32541 cdleme31so 33958 cdleme31se 33961 cdleme31sc 33963 cdleme31sde 33964 cdleme31sn2 33968 cdlemeg47rv2 34089 cdlemk41 34499 mapdheq 35308 hdmap1eq 35382 hdmapval2lem 35414 monotuz 35801 oddcomabszz 35804 fprodsplit1 37683 dvnmul 37828 sge0sn 38231 hoidmvlelem3 38429 riotaeqimp 39047 |
Copyright terms: Public domain | W3C validator |