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

Theorem nfcv 2258
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 1493 . 2  |-  F/ x  y  e.  A
21nfci 2248 1  |-  F/_ x A
Colors of variables: wff set class
Syntax hints:    e. wcel 1465   F/_wnfc 2245
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1410  ax-17 1491
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-nfc 2247
This theorem is referenced by:  nfcvd  2259  nfel  2267  nfeq1  2268  nfel1  2269  nfeq2  2270  nfel2  2271  nfcvf  2280  r2al  2431  r2ex  2432  nfraldxy  2444  nfrexdxy  2445  nfra2xy  2452  r19.12  2515  ralcom  2571  rexcom  2572  nfreudxy  2581  raleq  2603  rexeq  2604  reueq1  2605  rmoeq1  2606  cbvral  2627  cbvrex  2628  rabeq  2652  rabeqi  2653  cbvrabv  2659  vtoclg  2720  vtocl2g  2724  vtoclga  2726  vtocl2ga  2728  vtocl3ga  2730  spcimdv  2744  spcimedv  2746  spcgv  2747  spcegv  2748  rspct  2756  rspc  2757  rspce  2758  rspc2  2774  ceqsexg  2787  elabgt  2799  elabf  2801  elabg  2803  elab3g  2808  elrab  2813  mob  2839  nfsbc1v  2900  elrabsf  2919  sbcralt  2957  sbcrext  2958  sbcralg  2959  sbcrex  2960  sbcreug  2961  cbvcsbv  2980  csbconstg  2987  nfcsb1v  3005  csbie  3015  csbnestg  3024  cbvralcsf  3032  cbvrexcsf  3033  cbvreucsf  3034  cbvrabcsf  3035  cbvralv2  3036  cbvrexv2  3037  dfss4st  3279  n0rf  3345  n0r  3346  eq0  3351  raaanlem  3438  nfpw  3493  cbviunv  3822  cbviinv  3823  ssiun2s  3827  iunab  3829  ssiinf  3832  ssiin  3833  iinab  3844  cbvdisjv  3887  nfdisjv  3888  disjnims  3891  disji2  3892  cbvmptv  3994  triun  4009  csbexga  4026  repizf2  4056  moop2  4143  euotd  4146  opelopabf  4166  nfpo  4193  nfso  4194  pofun  4204  nfse  4233  nffrfor  4240  nffr  4241  frind  4244  nfwe  4247  eusvnf  4344  rabxfrd  4360  tfis  4467  tfisi  4471  opeliunxp  4564  nfrel  4594  opeliunxp2  4649  ralxpf  4655  rexxpf  4656  nfco  4674  nfcnv  4688  dfdmf  4702  dfrnf  4750  nfdm  4753  nfres  4791  resmptf  4839  nfiotadxy  5061  dffun6f  5106  dffun6  5107  dffun4f  5109  nffun  5116  funimaexglem  5176  nffv  5399  nffvmpt1  5400  dffn5imf  5444  funfvdm2f  5454  fvmptss2  5464  fvmpts  5467  fvmpt2  5472  fvmptssdm  5473  mptfvex  5474  fvmptdv  5477  fvmptd3  5482  elfvmptrab1  5483  eqfnfv2f  5490  ralrnmpt  5530  rexrnmpt  5531  f1ompt  5539  ffnfvf  5547  fmptco  5554  fmptcof  5555  fmptcos  5556  funiunfvdmf  5633  dff13f  5639  f1mpt  5640  fliftfuns  5667  nfiso  5675  nfriotadxy  5706  csbriotag  5710  riota2  5720  mpoeq123  5798  cbvmpox  5817  cbvmpo  5818  cbvmpov  5819  ovmpos  5862  ov2gf  5863  ovmpodxf  5864  ovmpodx  5865  ovmpodv  5871  ovmpodv2  5872  ovi3  5875  nfof  5955  nfofr  5956  offval2  5965  ofrfval2  5966  abrexex2g  5986  abrexex2  5990  dfopab2  6055  dfoprab3s  6056  mpomptsx  6063  dmmpossx  6065  fmpox  6066  mpofvex  6069  fnmpoovd  6080  fmpoco  6081  dfmpo  6088  f1od2  6100  disjxp1  6101  mpoxopoveq  6105  mpoxopovel  6106  nftpos  6144  tposoprab  6145  nfrecs  6172  nffrec  6261  eqerlem  6428  qliftfuns  6481  cbvixpv  6578  nfixpxy  6579  nfixp1  6580  ixpf  6582  mptelixpg  6596  dom2lem  6634  xpcomco  6688  xpf1o  6706  mapxpen  6710  ac6sfi  6760  nfsup  6847  nfdju  6895  exmidomni  6982  ismkvnex  6997  caucvgprprlemaddq  7484  caucvgsrlemgt1  7571  axpre-suploclemres  7677  lble  8669  supinfneg  9346  infsupneg  9347  fzrevral  9840  nfseq  10183  seq3f1olemstep  10229  seq3f1olemp  10230  fimaxre2  10953  nfsum1  11080  nfsum  11081  cbvsumv  11085  cbvsumi  11086  sumfct  11098  sumrbdclem  11100  summodclem2a  11105  zsumdc  11108  fsum3  11111  isumss  11115  isumss2  11117  fsum3cvg2  11118  fsumzcl2  11129  fsumadd  11130  fsumsplitf  11132  sumsnf  11133  sumsn  11135  sumsns  11139  fsumsplitsnun  11143  fsum2dlemstep  11158  fisumcom2  11162  fsumshftm  11169  fsum00  11186  fsumrelem  11195  fsumiun  11201  mertenslem2  11260  zsupcllemstep  11550  infssuzex  11554  infssuzcldc  11556  bezoutlemmain  11598  bezout  11611  prmind2  11713  oddpwdclemdvds  11759  oddpwdclemndvds  11760  ctiunctlemudc  11861  ctiunctlemf  11862  ctiunctlemfo  11863  ctiunct  11864  cnmpt11  12363  cnmpt1t  12365  cnmpt21  12371  cnmpt2t  12373  cnmptcom  12378  imasnopn  12379  fsumcncntop  12636  ellimc3apf  12709  ellimc3ap  12710  limcmpted  12712  elabf1  12884  elabf2  12885  elabg2  12888  bj-omssind  13029  bj-bdfindisg  13042  bj-nntrans  13045  bj-nnelirr  13047  bj-omtrans  13050  setindis  13061  bdsetindis  13063  bj-nn0sucALT  13072  bj-findis  13073  bj-findisg  13074  strcollnfALT  13080  isomninnlem  13121  trilpolemeq1  13129
  Copyright terms: Public domain W3C validator