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 2977 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | 1 | a1i 11 | 1 ⊢ (𝜑 → Ⅎ𝑥𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Ⅎwnfc 2961 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-5 1911 |
This theorem depends on definitions: df-bi 209 df-ex 1781 df-nf 1785 df-nfc 2963 |
This theorem is referenced by: nfeld 2989 nfraldw 3223 ralcom2 3363 nfreuw 3374 nfrmow 3375 vtoclgft 3553 vtoclgftOLD 3554 vtocld 3556 sbcralt 3855 sbcrext 3856 csbied 3919 csbie2t 3921 sbcco3gw 4374 sbcco3g 4379 csbco3g 4380 dfnfc2 4860 nfdisjw 5043 eusvnfb 5294 eusv2i 5295 dfid3 5462 iota2d 6343 iota2 6344 fmptcof 6892 nfriotadw 7122 riotaeqimp 7140 riota5f 7142 riota5 7143 oprabid 7188 opiota 7757 fmpoco 7790 axrepndlem1 10014 axrepndlem2 10015 axunnd 10018 axpowndlem2 10020 axpowndlem3 10021 axpowndlem4 10022 axpownd 10023 axregndlem2 10025 axinfndlem1 10027 axinfnd 10028 axacndlem4 10032 axacndlem5 10033 axacnd 10034 nfnegd 10881 prodsn 15316 fprodeq0g 15348 bpolylem 15402 pcmpt 16228 chfacfpmmulfsupp 21471 elmptrab 22435 dvfsumrlim3 24630 itgsubstlem 24645 itgsubst 24646 ifeqeqx 30297 disjunsn 30344 unirep 35003 riotasv2d 36108 cdleme31so 37530 cdleme31se 37533 cdleme31sc 37535 cdleme31sde 37536 cdleme31sn2 37540 cdlemeg47rv2 37661 cdlemk41 38071 mapdheq 38879 hdmap1eq 38952 hdmapval2lem 38982 monotuz 39558 oddcomabszz 39561 nfxnegd 41735 fprodsplit1 41894 dvnmul 42248 sge0sn 42681 hoidmvlelem3 42899 |
Copyright terms: Public domain | W3C validator |