Theorem nfcvd 2751

Description: If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 7-Oct-2016.)

Assertion

Ref	Expression
nfcvd	⊢ (𝜑 → Ⅎ𝑥𝐴)

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem nfcvd

Step	Hyp	Ref	Expression
1		nfcv 2750	. 2 ⊢ Ⅎ𝑥𝐴
2	1	a1i 11	1 ⊢ (𝜑 → Ⅎ𝑥𝐴)

Syntax hints:   → wi 4  Ⅎwnfc 2737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-5 1826

This theorem depends on definitions:  df-bi 195  df-ex 1695  df-nf 1700  df-nfc 2739

This theorem is referenced by:  nfeld  2758  ralcom2  3082  vtoclgft  3226  vtoclgftOLD  3227  vtocld  3229  sbcralt  3476  sbcrext  3477  sbcrextOLD  3478  csbied  3525  csbie2t  3527  sbcco3g  3950  csbco3g  3951  dfnfc2  4384  dfnfc2OLD  4385  eusvnfb  4783  eusv2i  4784  dfid3  4944  nfiotad  5757  iota2d  5779  iota2  5780  fmptcof  6289  riota5f  6513  riota5  6514  oprabid  6554  opiota  7096  fmpt2co  7125  axrepndlem1  9271  axrepndlem2  9272  axunnd  9275  axpowndlem2  9277  axpowndlem3  9278  axpowndlem4  9279  axpownd  9280  axregndlem2  9282  axinfndlem1  9284  axinfnd  9285  axacndlem4  9289  axacndlem5  9290  axacnd  9291  nfnegd  10128  sumsn  14268  prodsn  14480  fprodeq0g  14513  bpolylem  14567  pcmpt  15383  chfacfpmmulfsupp  20435  elmptrab  21388  dvfsumrlim3  23545  itgsubstlem  23560  itgsubst  23561  ifeqeqx  28579  disjunsn  28623  unirep  32501  riotasv2d  33085  cdleme31so  34509  cdleme31se  34512  cdleme31sc  34514  cdleme31sde  34515  cdleme31sn2  34519  cdlemeg47rv2  34640  cdlemk41  35050  mapdheq  35859  hdmap1eq  35933  hdmapval2lem  35965  monotuz  36348  oddcomabszz  36351  fprodsplit1  38484  dvnmul  38657  sge0sn  39096  hoidmvlelem3  39311  riotaeqimp  40185