ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfcv Unicode version

Theorem nfcv 2194
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.
StepHypRef Expression
1 nfv 1437 . 2  |-  F/ x  y  e.  A
21nfci 2184 1  |-  F/_ x A
Colors of variables: wff set class
Syntax hints:    e. wcel 1409   F/_wnfc 2181
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-gen 1354  ax-17 1435
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-nfc 2183
This theorem is referenced by:  nfcvd  2195  nfel  2202  nfeq1  2203  nfel1  2204  nfeq2  2205  nfel2  2206  nfcvf  2215  r2al  2360  r2ex  2361  nfraldxy  2373  nfrexdxy  2374  nfra2xy  2381  r19.12  2439  ralcom  2490  rexcom  2491  nfreudxy  2500  raleq  2522  rexeq  2523  reueq1  2524  rmoeq1  2525  cbvral  2546  cbvrex  2547  rabeq  2568  cbvrabv  2573  vtoclg  2630  vtocl2g  2634  vtoclga  2636  vtocl2ga  2638  vtocl3ga  2640  spcimdv  2654  spcimedv  2656  spcgv  2657  spcegv  2658  rspct  2666  rspc  2667  rspce  2668  rspc2  2683  ceqsexg  2694  elabgt  2706  elabf  2708  elabg  2710  elab3g  2715  elrab  2720  mob  2745  nfsbc1v  2804  elrabsf  2823  sbcralt  2861  sbcrext  2862  sbcralg  2863  sbcrex  2864  sbcreug  2865  cbvcsbv  2884  csbconstg  2891  nfcsb1v  2909  csbnestg  2927  cbvralcsf  2935  cbvrexcsf  2936  cbvreucsf  2937  cbvrabcsf  2938  cbvralv2  2939  cbvrexv2  2940  n0rf  3260  n0r  3261  eq0  3266  raaanlem  3353  nfpw  3398  cbviunv  3723  cbviinv  3724  ssiun2s  3728  iunab  3730  ssiinf  3733  ssiin  3734  iinab  3745  cbvdisjv  3783  nfdisjv  3784  cbvmptv  3879  triun  3894  csbexga  3912  repizf2  3942  moop2  4015  euotd  4018  opelopabf  4038  nfpo  4065  nfso  4066  pofun  4076  nfse  4105  nffrfor  4112  nffr  4113  frind  4116  nfwe  4119  eusvnf  4212  rabxfrd  4228  tfis  4333  tfisi  4337  opeliunxp  4422  nfrel  4452  opeliunxp2  4503  ralxpf  4509  rexxpf  4510  nfco  4528  nfcnv  4541  dfdmf  4555  dfrnf  4602  nfdm  4605  nfres  4641  nfiotadxy  4897  dffun6f  4942  dffun6  4943  dffun4f  4945  nffun  4951  funimaexglem  5009  nffv  5212  nffvmpt1  5213  dffn5imf  5255  funfvdm2f  5265  fvmptss2  5274  fvmpts  5277  fvmpt2  5281  fvmptssdm  5282  mptfvex  5283  fvmptdv  5286  eqfnfv2f  5296  ralrnmpt  5336  rexrnmpt  5337  f1ompt  5347  ffnfvf  5351  fmptco  5357  fmptcof  5358  fmptcos  5359  funiunfvdmf  5430  dff13f  5436  f1mpt  5437  fliftfuns  5465  nfiso  5473  nfriotadxy  5503  csbriotag  5507  riota2  5517  mpt2eq123  5591  cbvmpt2x  5609  cbvmpt2  5610  cbvmpt2v  5611  ovmpt2s  5651  ov2gf  5652  ovmpt2dxf  5653  ovmpt2dx  5654  ovmpt2dv  5660  ovmpt2dv2  5661  ovi3  5664  nfof  5744  nfofr  5745  offval2  5753  ofrfval2  5754  abrexex2g  5774  abrexex2  5778  dfopab2  5842  dfoprab3s  5843  mpt2mptsx  5850  dmmpt2ssx  5852  fmpt2x  5853  mpt2fvex  5856  fmpt2co  5864  dfmpt2  5871  f1od2  5883  mpt2xopoveq  5885  mpt2xopovel  5886  nftpos  5924  tposoprab  5925  nfrecs  5952  nffrec  6012  eqerlem  6167  qliftfuns  6220  dom2lem  6282  xpcomco  6330  ac6sfi  6382  nfsup  6397  caucvgprprlemaddq  6863  caucvgsrlemgt1  6936  fzrevral  9068  nfiseq  9381  nfsum1  10105  nfsum  10106  oddpwdclemdvds  10237  oddpwdclemndvds  10238  elabf1  10286  elabf2  10287  elabg2  10290  bj-omssind  10425  bj-bdfindisg  10439  bj-nntrans  10442  bj-nnelirr  10444  bj-omtrans  10447  setindis  10458  bdsetindis  10460  bj-nn0sucALT  10469  bj-findis  10470  bj-findisg  10471  strcollnfALT  10477
  Copyright terms: Public domain W3C validator