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

Theorem nfcv 2220
 Description: If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfcv 𝑥𝐴
Distinct variable group:   𝑥,𝐴

Proof of Theorem nfcv
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 nfv 1462 . 2 𝑥 𝑦𝐴
21nfci 2210 1 𝑥𝐴
 Colors of variables: wff set class Syntax hints:   ∈ wcel 1434  Ⅎwnfc 2207 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 1379  ax-17 1460 This theorem depends on definitions:  df-bi 115  df-nf 1391  df-nfc 2209 This theorem is referenced by:  nfcvd  2221  nfel  2228  nfeq1  2229  nfel1  2230  nfeq2  2231  nfel2  2232  nfcvf  2241  r2al  2386  r2ex  2387  nfraldxy  2399  nfrexdxy  2400  nfra2xy  2407  r19.12  2467  ralcom  2518  rexcom  2519  nfreudxy  2528  raleq  2550  rexeq  2551  reueq1  2552  rmoeq1  2553  cbvral  2574  cbvrex  2575  rabeq  2596  cbvrabv  2601  vtoclg  2659  vtocl2g  2663  vtoclga  2665  vtocl2ga  2667  vtocl3ga  2669  spcimdv  2683  spcimedv  2685  spcgv  2686  spcegv  2687  rspct  2695  rspc  2696  rspce  2697  rspc2  2712  ceqsexg  2724  elabgt  2736  elabf  2738  elabg  2740  elab3g  2745  elrab  2750  mob  2775  nfsbc1v  2834  elrabsf  2853  sbcralt  2891  sbcrext  2892  sbcralg  2893  sbcrex  2894  sbcreug  2895  cbvcsbv  2914  csbconstg  2921  nfcsb1v  2939  csbnestg  2957  cbvralcsf  2965  cbvrexcsf  2966  cbvreucsf  2967  cbvrabcsf  2968  cbvralv2  2969  cbvrexv2  2970  n0rf  3267  n0r  3268  eq0  3273  raaanlem  3354  nfpw  3402  cbviunv  3725  cbviinv  3726  ssiun2s  3730  iunab  3732  ssiinf  3735  ssiin  3736  iinab  3747  cbvdisjv  3785  nfdisjv  3786  cbvmptv  3881  triun  3896  csbexga  3914  repizf2  3944  moop2  4014  euotd  4017  opelopabf  4037  nfpo  4064  nfso  4065  pofun  4075  nfse  4104  nffrfor  4111  nffr  4112  frind  4115  nfwe  4118  eusvnf  4211  rabxfrd  4227  tfis  4332  tfisi  4336  opeliunxp  4421  nfrel  4451  opeliunxp2  4504  ralxpf  4510  rexxpf  4511  nfco  4529  nfcnv  4542  dfdmf  4556  dfrnf  4603  nfdm  4606  nfres  4642  nfiotadxy  4900  dffun6f  4945  dffun6  4946  dffun4f  4948  nffun  4954  funimaexglem  5013  nffv  5216  nffvmpt1  5217  dffn5imf  5260  funfvdm2f  5270  fvmptss2  5279  fvmpts  5282  fvmpt2  5286  fvmptssdm  5287  mptfvex  5288  fvmptdv  5291  eqfnfv2f  5301  ralrnmpt  5341  rexrnmpt  5342  f1ompt  5352  ffnfvf  5356  fmptco  5362  fmptcof  5363  fmptcos  5364  funiunfvdmf  5435  dff13f  5441  f1mpt  5442  fliftfuns  5469  nfiso  5477  nfriotadxy  5507  csbriotag  5511  riota2  5521  mpt2eq123  5595  cbvmpt2x  5613  cbvmpt2  5614  cbvmpt2v  5615  ovmpt2s  5655  ov2gf  5656  ovmpt2dxf  5657  ovmpt2dx  5658  ovmpt2dv  5664  ovmpt2dv2  5665  ovi3  5668  nfof  5748  nfofr  5749  offval2  5757  ofrfval2  5758  abrexex2g  5778  abrexex2  5782  dfopab2  5846  dfoprab3s  5847  mpt2mptsx  5854  dmmpt2ssx  5856  fmpt2x  5857  mpt2fvex  5860  fmpt2co  5868  dfmpt2  5875  f1od2  5887  mpt2xopoveq  5889  mpt2xopovel  5890  nftpos  5928  tposoprab  5929  nfrecs  5956  nffrec  6045  eqerlem  6203  qliftfuns  6256  dom2lem  6319  xpcomco  6370  xpf1o  6385  ac6sfi  6431  nfsup  6464  caucvgprprlemaddq  6960  caucvgsrlemgt1  7033  lble  8092  supinfneg  8764  infsupneg  8765  fzrevral  9198  nfiseq  9528  fimaxre2  10247  nfsum1  10331  nfsum  10332  zsupcllemstep  10485  infssuzex  10489  infssuzcldc  10491  bezoutlemmain  10531  bezout  10544  prmind2  10646  oddpwdclemdvds  10692  oddpwdclemndvds  10693  elabf1  10742  elabf2  10743  elabg2  10746  bj-omssind  10888  bj-bdfindisg  10901  bj-nntrans  10904  bj-nnelirr  10906  bj-omtrans  10909  setindis  10920  bdsetindis  10922  bj-nn0sucALT  10931  bj-findis  10932  bj-findisg  10933  strcollnfALT  10939
 Copyright terms: Public domain W3C validator