Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nfcvd | Structured version Visualization version Unicode version |
Description: If is disjoint from , then is not free in . (Contributed by Mario Carneiro, 7-Oct-2016.) |
Ref | Expression |
---|---|
nfcvd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2764 | . 2 | |
2 | 1 | a1i 11 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wnfc 2751 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-5 1839 |
This theorem depends on definitions: df-bi 197 df-ex 1705 df-nf 1710 df-nfc 2753 |
This theorem is referenced by: nfeld 2773 ralcom2 3104 vtoclgft 3254 vtoclgftOLD 3255 vtocld 3257 sbcralt 3510 sbcrext 3511 sbcrextOLD 3512 csbied 3560 csbie2t 3562 sbcco3g 3999 csbco3g 4000 dfnfc2 4454 dfnfc2OLD 4455 eusvnfb 4862 eusv2i 4863 dfid3 5025 iota2d 5876 iota2 5877 fmptcof 6397 riotaeqimp 6634 riota5f 6636 riota5 6637 oprabid 6677 opiota 7229 fmpt2co 7260 axrepndlem1 9414 axrepndlem2 9415 axunnd 9418 axpowndlem2 9420 axpowndlem3 9421 axpowndlem4 9422 axpownd 9423 axregndlem2 9425 axinfndlem1 9427 axinfnd 9428 axacndlem4 9432 axacndlem5 9433 axacnd 9434 nfnegd 10276 sumsn 14475 prodsn 14692 fprodeq0g 14725 bpolylem 14779 pcmpt 15596 chfacfpmmulfsupp 20668 elmptrab 21630 dvfsumrlim3 23796 itgsubstlem 23811 itgsubst 23812 ifeqeqx 29361 disjunsn 29407 unirep 33507 riotasv2d 34243 cdleme31so 35667 cdleme31se 35670 cdleme31sc 35672 cdleme31sde 35673 cdleme31sn2 35677 cdlemeg47rv2 35798 cdlemk41 36208 mapdheq 37017 hdmap1eq 37091 hdmapval2lem 37123 monotuz 37506 oddcomabszz 37509 nfxnegd 39668 fprodsplit1 39825 dvnmul 40158 sge0sn 40596 hoidmvlelem3 40811 |
Copyright terms: Public domain | W3C validator |