![]() |
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 2912 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | 1 | a1i 11 | 1 ⊢ (𝜑 → Ⅎ𝑥𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Ⅎwnfc 2899 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-5 1990 |
This theorem depends on definitions: df-bi 197 df-ex 1852 df-nf 1857 df-nfc 2901 |
This theorem is referenced by: nfeld 2921 ralcom2 3251 vtoclgft 3403 vtoclgftOLD 3404 vtocld 3406 sbcralt 3658 sbcrext 3659 csbied 3707 csbie2t 3709 sbcco3g 4141 csbco3g 4142 dfnfc2 4590 eusvnfb 4990 eusv2i 4991 dfid3 5158 iota2d 6019 iota2 6020 fmptcof 6539 riotaeqimp 6776 riota5f 6778 riota5 6779 oprabid 6821 opiota 7377 fmpt2co 7410 axrepndlem1 9615 axrepndlem2 9616 axunnd 9619 axpowndlem2 9621 axpowndlem3 9622 axpowndlem4 9623 axpownd 9624 axregndlem2 9626 axinfndlem1 9628 axinfnd 9629 axacndlem4 9633 axacndlem5 9634 axacnd 9635 nfnegd 10477 sumsn 14682 prodsn 14898 fprodeq0g 14930 bpolylem 14984 pcmpt 15802 chfacfpmmulfsupp 20887 elmptrab 21850 dvfsumrlim3 24015 itgsubstlem 24030 itgsubst 24031 ifeqeqx 29693 disjunsn 29739 unirep 33832 riotasv2d 34758 cdleme31so 36181 cdleme31se 36184 cdleme31sc 36186 cdleme31sde 36187 cdleme31sn2 36191 cdlemeg47rv2 36312 cdlemk41 36722 mapdheq 37531 hdmap1eq 37604 hdmapval2lem 37634 monotuz 38025 oddcomabszz 38028 nfxnegd 40178 fprodsplit1 40337 dvnmul 40670 sge0sn 41107 hoidmvlelem3 41325 |
Copyright terms: Public domain | W3C validator |