![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfcvd | Structured version Visualization version GIF 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 2793 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | 1 | a1i 11 | 1 ⊢ (𝜑 → Ⅎ𝑥𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Ⅎwnfc 2780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-5 1879 |
This theorem depends on definitions: df-bi 197 df-ex 1745 df-nf 1750 df-nfc 2782 |
This theorem is referenced by: nfeld 2802 ralcom2 3133 vtoclgft 3285 vtoclgftOLD 3286 vtocld 3288 sbcralt 3543 sbcrext 3544 sbcrextOLD 3545 csbied 3593 csbie2t 3595 sbcco3g 4032 csbco3g 4033 dfnfc2 4486 dfnfc2OLD 4487 eusvnfb 4892 eusv2i 4893 dfid3 5054 iota2d 5914 iota2 5915 fmptcof 6437 riotaeqimp 6674 riota5f 6676 riota5 6677 oprabid 6717 opiota 7273 fmpt2co 7305 axrepndlem1 9452 axrepndlem2 9453 axunnd 9456 axpowndlem2 9458 axpowndlem3 9459 axpowndlem4 9460 axpownd 9461 axregndlem2 9463 axinfndlem1 9465 axinfnd 9466 axacndlem4 9470 axacndlem5 9471 axacnd 9472 nfnegd 10314 sumsn 14519 prodsn 14736 fprodeq0g 14769 bpolylem 14823 pcmpt 15643 chfacfpmmulfsupp 20716 elmptrab 21678 dvfsumrlim3 23841 itgsubstlem 23856 itgsubst 23857 ifeqeqx 29487 disjunsn 29533 unirep 33637 riotasv2d 34561 cdleme31so 35984 cdleme31se 35987 cdleme31sc 35989 cdleme31sde 35990 cdleme31sn2 35994 cdlemeg47rv2 36115 cdlemk41 36525 mapdheq 37334 hdmap1eq 37408 hdmapval2lem 37440 monotuz 37823 oddcomabszz 37826 nfxnegd 39981 fprodsplit1 40143 dvnmul 40476 sge0sn 40914 hoidmvlelem3 41132 |
Copyright terms: Public domain | W3C validator |