| 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 2905 | . 2 ⊢ Ⅎ𝑥𝐴 | |
| 2 | 1 | a1i 11 | 1 ⊢ (𝜑 → Ⅎ𝑥𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 Ⅎwnfc 2890 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 df-nf 1784 df-nfc 2892 |
| This theorem is referenced by: nfeld 2917 ralcom2 3377 nfreuwOLD 3426 nfrmowOLD 3427 cbvexeqsetf 3495 sbcralt 3872 sbcrext 3873 csbie2t 3937 sbcco3gw 4425 sbcco3g 4430 csbco3g 4431 dfnfc2 4929 nfdisjw 5122 eusvnfb 5393 eusv2i 5394 dfid3 5581 iota2d 6549 iota2 6550 fmptcof 7150 nfriotadw 7396 riotaeqimp 7414 riota5f 7416 riota5 7417 oprabid 7463 opiota 8084 fmpoco 8120 nfttrcld 9750 axrepndlem1 10632 axrepndlem2 10633 axunnd 10636 axpowndlem2 10638 axpowndlem3 10639 axpowndlem4 10640 axpownd 10641 axregndlem2 10643 axinfndlem1 10645 axinfnd 10646 axacndlem4 10650 axacndlem5 10651 axacnd 10652 nfnegd 11503 prodsn 15998 fprodeq0g 16030 bpolylem 16084 pcmpt 16930 chfacfpmmulfsupp 22869 elmptrab 23835 dvfsumrlim3 26074 itgsubstlem 26089 itgsubst 26090 ifeqeqx 32555 disjunsn 32607 axnulg 35106 bj-elgab 36940 bj-gabima 36941 wl-issetft 37583 unirep 37721 riotasv2d 38958 cdleme31so 40381 cdleme31se 40384 cdleme31sc 40386 cdleme31sde 40387 cdleme31sn2 40391 cdlemeg47rv2 40512 cdlemk41 40922 mapdheq 41730 hdmap1eq 41803 hdmapval2lem 41833 monotuz 42953 oddcomabszz 42956 mnringvald 44227 nfxnegd 45452 fprodsplit1 45608 dvnmul 45958 sge0sn 46394 hoidmvlelem3 46612 |
| Copyright terms: Public domain | W3C validator |