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

Theorem nfcv 2225
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 1464 . 2  |-  F/ x  y  e.  A
21nfci 2215 1  |-  F/_ x A
Colors of variables: wff set class
Syntax hints:    e. wcel 1436   F/_wnfc 2212
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1381  ax-17 1462
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-nfc 2214
This theorem is referenced by:  nfcvd  2226  nfel  2233  nfeq1  2234  nfel1  2235  nfeq2  2236  nfel2  2237  nfcvf  2246  r2al  2393  r2ex  2394  nfraldxy  2406  nfrexdxy  2407  nfra2xy  2414  r19.12  2474  ralcom  2526  rexcom  2527  nfreudxy  2536  raleq  2558  rexeq  2559  reueq1  2560  rmoeq1  2561  cbvral  2582  cbvrex  2583  rabeq  2607  rabeqi  2608  cbvrabv  2614  vtoclg  2672  vtocl2g  2676  vtoclga  2678  vtocl2ga  2680  vtocl3ga  2682  spcimdv  2696  spcimedv  2698  spcgv  2699  spcegv  2700  rspct  2708  rspc  2709  rspce  2710  rspc2  2724  ceqsexg  2736  elabgt  2748  elabf  2750  elabg  2752  elab3g  2757  elrab  2762  mob  2788  nfsbc1v  2847  elrabsf  2866  sbcralt  2904  sbcrext  2905  sbcralg  2906  sbcrex  2907  sbcreug  2908  cbvcsbv  2927  csbconstg  2934  nfcsb1v  2952  csbie  2962  csbnestg  2971  cbvralcsf  2979  cbvrexcsf  2980  cbvreucsf  2981  cbvrabcsf  2982  cbvralv2  2983  cbvrexv2  2984  dfss4st  3221  n0rf  3284  n0r  3285  eq0  3290  raaanlem  3374  nfpw  3427  cbviunv  3752  cbviinv  3753  ssiun2s  3757  iunab  3759  ssiinf  3762  ssiin  3763  iinab  3774  cbvdisjv  3812  nfdisjv  3813  cbvmptv  3908  triun  3923  csbexga  3941  repizf2  3971  moop2  4051  euotd  4054  opelopabf  4074  nfpo  4101  nfso  4102  pofun  4112  nfse  4141  nffrfor  4148  nffr  4149  frind  4152  nfwe  4155  eusvnf  4248  rabxfrd  4264  tfis  4370  tfisi  4374  opeliunxp  4460  nfrel  4490  opeliunxp2  4543  ralxpf  4549  rexxpf  4550  nfco  4568  nfcnv  4582  dfdmf  4596  dfrnf  4643  nfdm  4646  nfres  4682  nfiotadxy  4946  dffun6f  4991  dffun6  4992  dffun4f  4994  nffun  5000  funimaexglem  5059  nffv  5272  nffvmpt1  5273  dffn5imf  5316  funfvdm2f  5326  fvmptss2  5336  fvmpts  5339  fvmpt2  5343  fvmptssdm  5344  mptfvex  5345  fvmptdv  5348  eqfnfv2f  5358  ralrnmpt  5398  rexrnmpt  5399  f1ompt  5407  ffnfvf  5414  fmptco  5421  fmptcof  5422  fmptcos  5423  funiunfvdmf  5498  dff13f  5504  f1mpt  5505  fliftfuns  5532  nfiso  5540  nfriotadxy  5571  csbriotag  5575  riota2  5585  mpt2eq123  5659  cbvmpt2x  5677  cbvmpt2  5678  cbvmpt2v  5679  ovmpt2s  5719  ov2gf  5720  ovmpt2dxf  5721  ovmpt2dx  5722  ovmpt2dv  5728  ovmpt2dv2  5729  ovi3  5732  nfof  5812  nfofr  5813  offval2  5821  ofrfval2  5822  abrexex2g  5842  abrexex2  5846  dfopab2  5910  dfoprab3s  5911  mpt2mptsx  5918  dmmpt2ssx  5920  fmpt2x  5921  mpt2fvex  5924  fmpt2co  5932  dfmpt2  5939  f1od2  5951  mpt2xopoveq  5953  mpt2xopovel  5954  nftpos  5992  tposoprab  5993  nfrecs  6020  nffrec  6109  eqerlem  6269  qliftfuns  6322  dom2lem  6435  xpcomco  6488  xpf1o  6506  mapxpen  6510  ac6sfi  6560  nfsup  6624  nfdju  6672  exmidomni  6735  caucvgprprlemaddq  7204  caucvgsrlemgt1  7277  lble  8336  supinfneg  9008  infsupneg  9009  fzrevral  9442  nfiseq  9779  iseqf1olemstep  9827  iseqf1olemp  9828  fimaxre2  10544  nfsum1  10628  nfsum  10629  cbvsumv  10633  cbvsumi  10634  sumfct  10646  isumrblem  10648  isummolem2a  10653  zisum  10656  fisum  10658  isumss  10662  zsupcllemstep  10808  infssuzex  10812  infssuzcldc  10814  bezoutlemmain  10854  bezout  10867  prmind2  10969  oddpwdclemdvds  11015  oddpwdclemndvds  11016  elabf1  11111  elabf2  11112  elabg2  11115  bj-omssind  11260  bj-bdfindisg  11273  bj-nntrans  11276  bj-nnelirr  11278  bj-omtrans  11281  setindis  11292  bdsetindis  11294  bj-nn0sucALT  11303  bj-findis  11304  bj-findisg  11305  strcollnfALT  11311
  Copyright terms: Public domain W3C validator