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

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

Proof of Theorem nfcv
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 nfv 1398 . 2  F/
21nfci 2146 1  F/_
Colors of variables: wff set class
Syntax hints:   wcel 1370   F/_wnfc 2143
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1314  ax-17 1396
This theorem depends on definitions:  df-bi 110  df-nf 1326  df-nfc 2145
This theorem is referenced by:  nfcvd  2157  nfel  2164  nfeq1  2165  nfel1  2166  nfeq2  2167  nfel2  2168  nfcvf  2177  r2al  2317  r2ex  2318  nfraldxy  2330  nfrexdxy  2331  nfra2xy  2338  r19.12  2396  ralcom  2447  rexcom  2448  nfreudxy  2457  raleq  2479  rexeq  2480  reueq1  2481  rmoeq1  2482  cbvral  2503  cbvrex  2504  rabeq  2525  cbvrabv  2530  vtoclg  2586  vtocl2g  2590  vtoclga  2592  vtocl2ga  2594  vtocl3ga  2596  spcimdv  2610  spcimedv  2612  spcgv  2613  spcegv  2614  rspct  2622  rspc  2623  rspce  2624  rspc2  2634  ceqsexg  2645  elabgt  2657  elabf  2659  elabg  2661  elab3g  2666  elrab  2671  mob  2696  nfsbc1v  2755  elrabsf  2774  sbcralt  2807  sbcrext  2808  sbcralg  2809  sbcrexg  2810  sbcreug  2811  cbvcsbv  2830  csbconstg  2837  nfcsb1v  2855  csbnestg  2873  cbvralcsf  2881  cbvrexcsf  2882  cbvreucsf  2883  cbvrabcsf  2884  cbvralv2  2885  cbvrexv2  2886  n0rf  3206  n0r  3207  eq0  3212  raaanlem  3301  nfpw  3342  cbviunv  3666  cbviinv  3667  ssiun2s  3671  iunab  3673  ssiinf  3676  ssiin  3677  iinab  3688  cbvdisjv  3726  nfdisjv  3727  cbvmptv  3822  triun  3837  csbexgOLD  3855  repizf2  3885  moop2  3958  euotd  3961  opelopabf  3981  nfpo  4008  nfso  4009  pofun  4019  nfse  4042  eusvnf  4131  rabxfrd  4147  tfis  4229  tfisi  4233  opeliunxp  4318  nfrel  4348  opeliunxp2  4399  ralxpf  4405  rexxpf  4406  nfco  4424  nfcnv  4437  dfdmf  4451  dfrnf  4498  nfdm  4501  nfres  4537  nfiotadxy  4793  dffun6f  4837  dffun6  4838  dffun4f  4840  nffun  4846  funimaexglem  4904  nffv  5106  nffvmpt1  5107  dffn5imf  5149  funfvdm2f  5159  fvmptss2  5168  fvmpts  5171  fvmpt2  5175  fvmptssdm  5176  mptfvex  5177  fvmptdv  5180  eqfnfv2f  5190  ralrnmpt  5230  rexrnmpt  5231  f1ompt  5241  ffnfvf  5245  fmptco  5251  fmptcof  5252  fmptcos  5253  funiunfvdmf  5324  dff13f  5330  f1mpt  5331  fliftfuns  5359  nfiso  5367  nfriotadxy  5396  csbriotag  5400  riota2  5410  mpt2eq123  5483  cbvmpt2x  5501  cbvmpt2  5502  cbvmpt2v  5503  ovmpt2s  5543  ov2gf  5544  ovmpt2dxf  5545  ovmpt2dx  5546  ovmpt2dv  5552  ovmpt2dv2  5553  ovi3  5556  nfof  5636  nfofr  5637  offval2  5645  ofrfval2  5646  abrexex2g  5666  abrexex2  5670  dfopab2  5734  dfoprab3s  5735  mpt2mptsx  5742  dmmpt2ssx  5744  fmpt2x  5745  mpt2fvex  5748  fmpt2co  5756  dfmpt2  5763  mpt2xopoveq  5773  mpt2xopovel  5774  nftpos  5812  tposoprab  5813  nfrecs  5840  eqerlem  6044  qliftfuns  6097  elabf1  7219  elabf2  7220  elabg2  7223  bj-omssind  7353  bj-bdfindisg  7366  bj-nntrans  7369  bj-nnelirr  7371  bj-omtrans  7374  setindis  7381  bdsetindis  7383  bj-nn0sucALT  7392  bj-findis  7393  bj-findisg  7394  strcollnfALT  7400
  Copyright terms: Public domain W3C validator