Theorem nfcvd 2896

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 2895	. 2 ⊢ Ⅎ𝑥𝐴
2	1	a1i 11	1 ⊢ (𝜑 → Ⅎ𝑥𝐴)

Syntax hints:   → wi 4  Ⅎwnfc 2880

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 207  df-ex 1781  df-nf 1785  df-nfc 2882

This theorem is referenced by:  nfeld  2907  ralcom2  3344  cbvexeqsetf  3452  sbcralt  3819  sbcrext  3820  csbie2t  3884  sbcco3gw  4374  sbcco3g  4379  csbco3g  4380  dfnfc2  4880  nfdisjw  5072  eusvnfb  5333  eusv2i  5334  dfid3  5517  iota2d  6474  iota2  6475  fmptcof  7069  nfriotadw  7317  riotaeqimp  7335  riota5f  7337  riota5  7338  oprabid  7384  opiota  7997  fmpoco  8031  nfttrcld  9607  axrepndlem1  10490  axrepndlem2  10491  axunnd  10494  axpowndlem2  10496  axpowndlem3  10497  axpowndlem4  10498  axpownd  10499  axregndlem2  10501  axinfndlem1  10503  axinfnd  10504  axacndlem4  10508  axacndlem5  10509  axacnd  10510  nfnegd  11362  prodsn  15871  fprodeq0g  15903  bpolylem  15957  pcmpt  16806  nfchnd  18519  chfacfpmmulfsupp  22779  elmptrab  23743  dvfsumrlim3  25968  itgsubstlem  25983  itgsubst  25984  ifeqeqx  32524  disjunsn  32576  axnulg  35140  bj-elgab  37004  bj-gabima  37005  wl-issetft  37647  unirep  37774  riotasv2d  39076  cdleme31so  40498  cdleme31se  40501  cdleme31sc  40503  cdleme31sde  40504  cdleme31sn2  40508  cdlemeg47rv2  40629  cdlemk41  41039  mapdheq  41847  hdmap1eq  41920  hdmapval2lem  41950  monotuz  43058  oddcomabszz  43061  mnringvald  44330  nfxnegd  45563  fprodsplit1  45717  dvnmul  46065  sge0sn  46501  hoidmvlelem3  46719