MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfcvd Structured version   Visualization version   GIF version

Theorem nfcvd 2908
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
StepHypRef Expression
1 nfcv 2907 . 2 𝑥𝐴
21a1i 11 1 (𝜑𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnfc 2894
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-5 2005
This theorem depends on definitions:  df-bi 198  df-ex 1875  df-nf 1879  df-nfc 2896
This theorem is referenced by:  nfeld  2916  ralcom2  3251  vtoclgft  3407  vtocld  3409  sbcralt  3669  sbcrext  3670  csbied  3718  csbie2t  3720  sbcco3g  4160  csbco3g  4161  dfnfc2  4614  eusvnfb  5028  eusv2i  5029  dfid3  5186  iota2d  6056  iota2  6057  fmptcof  6588  riotaeqimp  6826  riota5f  6828  riota5  6829  oprabid  6873  opiota  7429  fmpt2co  7462  axrepndlem1  9667  axrepndlem2  9668  axunnd  9671  axpowndlem2  9673  axpowndlem3  9674  axpowndlem4  9675  axpownd  9676  axregndlem2  9678  axinfndlem1  9680  axinfnd  9681  axacndlem4  9685  axacndlem5  9686  axacnd  9687  nfnegd  10530  prodsn  14975  fprodeq0g  15007  bpolylem  15061  pcmpt  15875  chfacfpmmulfsupp  20947  elmptrab  21910  dvfsumrlim3  24087  itgsubstlem  24102  itgsubst  24103  ifeqeqx  29810  disjunsn  29855  unirep  33930  riotasv2d  34913  cdleme31so  36335  cdleme31se  36338  cdleme31sc  36340  cdleme31sde  36341  cdleme31sn2  36345  cdlemeg47rv2  36466  cdlemk41  36876  mapdheq  37684  hdmap1eq  37757  hdmapval2lem  37787  monotuz  38183  oddcomabszz  38186  nfxnegd  40305  fprodsplit1  40463  dvnmul  40796  sge0sn  41233  hoidmvlelem3  41451
  Copyright terms: Public domain W3C validator