Theorem nfcv 2392

Description: If x is disjoint from A, then x is not free in A. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfcv	|- F/_ x A

Distinct variable group:   x, A

Proof of Theorem nfcv

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1581	. 2 |- F/ x y e. A
2	1	nfci 2382	1 |- F/_ x A

This proof depends on syntax axioms:   e. wcel 2209   F/_wnfc 2379

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-nfc 2381

This theorem is used by:  nfcvd  2393  nfel  2401  nfeq1  2402  nfel1  2403  nfeq2  2404  nfel2  2405  nfcvf  2415  r2al  2569  r2ex  2570  nfraldxy  2583  nfrexdxy  2584  nfra2xy  2592  r19.12  2657  ralcom  2714  rexcom  2715  nfreudxy  2725  raleq  2749  rexeq  2750  reueq1  2751  rmoeq1  2752  cbvralw  2779  cbvrexw  2780  cbvral  2782  cbvrex  2783  rabeq  2813  rabeqi  2814  cbvrabv  2820  vtoclg  2883  vtocl2g  2887  vtoclga  2889  vtocl2ga  2891  vtocl3ga  2893  spcimdv  2909  spcimedv  2911  spcgv  2912  spcegv  2913  rspct  2922  rspc  2923  rspce  2924  rspc2  2941  ceqsexg  2954  elabgt  2967  elabf  2969  elabg  2972  elab3g  2977  elrab  2982  mob  3008  nfsbc1v  3070  elrabsf  3090  sbcralt  3128  sbcrext  3129  sbcralg  3130  sbcrex  3131  sbcreug  3132  reu8nf  3133  cbvcsbv  3153  csbconstg  3161  nfcsb1v  3180  csbie  3193  csbnestg  3202  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  cbvralv2  3214  cbvrexv2  3215  dfss4st  3464  n0rf  3534  n0r  3535  eq0  3540  raaanlem  3632  nfpw  3705  cbviunv  4051  cbviinv  4052  ssiun2s  4056  iunab  4059  ssiinf  4062  ssiin  4063  iinab  4074  cbvdisjv  4117  nfdisjv  4118  disjnims  4121  disji2  4122  invdisjrab  4124  cbvmptv  4227  triun  4242  csbexga  4261  repizf2  4299  moop2  4392  euotd  4395  opelopabgf  4412  opelopabf  4417  nfpo  4446  nfso  4447  pofun  4457  nfse  4486  nffrfor  4493  nffr  4494  frind  4497  nfwe  4500  eusvnf  4599  rabxfrd  4615  tfis  4730  tfisi  4734  opeliunxp  4830  nfrel  4860  opeliunxp2  4920  ralxpf  4926  rexxpf  4927  nfco  4945  nfcnv  4959  dfdmf  4974  dfrnf  5023  nfdm  5026  nfres  5065  resmptf  5113  nfiotadw  5340  dffun6f  5390  dffun6  5391  dffun4f  5393  nffun  5400  funimaexglem  5464  nffv  5705  nffvmpt1  5706  dffn5imf  5758  funfvdm2f  5768  fvmptss2  5780  fvmpts  5783  fvmpt2  5789  fvmptssdm  5790  mptfvex  5791  fvmptdv  5794  fvmptd3  5799  elfvmptrab1  5801  eqfnfv2f  5810  ralrnmpt  5850  rexrnmpt  5851  f1ompt  5859  ffnfvf  5867  fmptco  5874  fmptcof  5875  fmptcos  5876  dfimafnf  5955  funiunfvdmf  5970  dff13f  5976  f1mpt  5977  fliftfuns  6004  nfiso  6012  nfriotadxy  6047  csbriotag  6052  riota2  6062  mpoeq123  6147  cbvmpox  6166  cbvmpo  6167  cbvmpov  6168  ovmpos  6212  ov2gf  6213  ovmpodxf  6214  ovmpodx  6215  ovmpodv  6221  ovmpodv2  6222  fvmpopr2d  6225  ovi3  6226  elovmporab  6289  elovmporab1w  6290  nfof  6308  nfofr  6309  offval2  6318  ofrfval2  6319  abrexex2g  6349  abrexex2  6353  uchoice  6371  dfopab2  6423  dfoprab3s  6424  mpomptsx  6433  dmmpossx  6435  fmpox  6436  mpofvex  6441  fnmpoovd  6451  fmpoco  6452  dfmpo  6459  f1od2  6471  disjxp1  6472  mpoxopoveq  6511  mpoxopovel  6512  nftpos  6550  tposoprab  6551  nfrecs  6578  nffrec  6667  eqerlem  6838  qliftfuns  6893  cbvixpv  6998  nfixpxy  6999  nfixp1  7000  ixpf  7002  mptelixpg  7016  dom2lem  7058  modom  7108  xpcomco  7124  xpf1o  7144  mapxpen  7148  ac6sfi  7202  opabfi  7247  nfsup  7333  nfdju  7383  exmidomni  7483  ismkvnex  7496  cc2  7634  cc4f  7636  cc4  7637  caucvgprprlemaddq  8076  caucvgsrlemgt1  8163  axpre-suploclemres  8269  lble  9280  supinfneg  10005  infsupneg  10006  fzrevral  10523  zsupcllemstep  10673  infssuzex  10677  infssuzcldc  10679  infssfzcldc  10680  infssfzledc  10681  nfseq  10908  seq3f1olemstep  10965  seq3f1olemp  10966  nfwrd  11348  reuccatpfxs1v  11535  fimaxre2  12009  nfsum1  12140  nfsum  12141  cbvsumv  12145  cbvsumi  12146  sumfct  12158  sumrbdclem  12162  summodclem2a  12166  zsumdc  12169  fsum3  12172  isumss  12176  isumss2  12178  fsum3cvg2  12179  fsumzcl2  12190  fsumadd  12191  fsumsplitf  12193  sumsnf  12194  sumsn  12196  sumsns  12200  fsumsplitsnun  12204  fsum2dlemstep  12219  fisumcom2  12223  fsumshftm  12230  fsum00  12247  fsumrelem  12256  fsumiun  12262  mertenslem2  12321  prodeq1  12338  nfcprod1  12339  nfcprod  12340  cbvprod  12343  cbvprodv  12344  cbvprodi  12345  prodrbdclem  12356  prodmodclem2a  12361  zproddc  12364  fprodseq  12368  fprodntrivap  12369  prodfct  12372  prodssdc  12374  prodsnf  12377  prodsn  12378  fprodm1s  12386  fprodp1s  12387  prodsns  12388  fprodcllemf  12398  fprodconst  12405  fprodap0  12406  fprod2dlemstep  12407  fprodcom2fi  12411  fprodrec  12414  fproddivapf  12416  fprodsplitf  12417  fprodap0f  12421  fprodle  12425  bezoutlemmain  12793  bezout  12806  nnwofdc  12833  nnwosdc  12834  prmind2  12916  nnmaxpwlemdvds  12967  nnmaxpwlemndvds  12968  pcmpt  13144  pcmptdvds  13146  ctiunctlemudc  13379  ctiunctlemf  13380  ctiunctlemfo  13381  ctiunct  13382  ctiunctal  13383  gzsumconstf  14195  gzsumsplit0  14199  gsumsncmn  14207  gsummptfidmadd  14212  prdsbas3  14238  cnmpt11  15436  cnmpt1t  15438  cnmpt21  15444  cnmpt2t  15446  cnmptcom  15451  imasnopn  15452  fsumcncntop  15720  ellimc3apf  15813  ellimc3ap  15814  limcmpted  15816  dvmptfsum  15878  elplyd  15894  fsumdvdsmul  16207  lgseisenlem2  16312  gropd  16410  grstructd2dom  16411  lfgrnloopen  16496  elabf1  16931  elabf2  16932  elabg2  16935  bj-omssind  17083  bj-bdfindisg  17096  bj-nntrans  17099  bj-nnelirr  17101  bj-omtrans  17104  setindis  17115  bdsetindis  17117  bj-nn0sucALT  17126  bj-findis  17127  bj-findisg  17128  strcollnfALT  17134  isomninnlem  17201  trilpolemeq1  17211  trirec0  17215  iswomninnlem  17221  ismkvnnlem  17224  nconstwlpolemgt0  17236