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

Theorem nfcv 2258
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 1493 . 2 𝑥 𝑦𝐴
21nfci 2248 1 𝑥𝐴
Colors of variables: wff set class
Syntax hints:  wcel 1465  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  8673  supinfneg  9358  infsupneg  9359  fzrevral  9853  nfseq  10196  seq3f1olemstep  10242  seq3f1olemp  10243  fimaxre2  10966  nfsum1  11093  nfsum  11094  cbvsumv  11098  cbvsumi  11099  sumfct  11111  sumrbdclem  11113  summodclem2a  11118  zsumdc  11121  fsum3  11124  isumss  11128  isumss2  11130  fsum3cvg2  11131  fsumzcl2  11142  fsumadd  11143  fsumsplitf  11145  sumsnf  11146  sumsn  11148  sumsns  11152  fsumsplitsnun  11156  fsum2dlemstep  11171  fisumcom2  11175  fsumshftm  11182  fsum00  11199  fsumrelem  11208  fsumiun  11214  mertenslem2  11273  zsupcllemstep  11565  infssuzex  11569  infssuzcldc  11571  bezoutlemmain  11613  bezout  11626  prmind2  11728  oddpwdclemdvds  11775  oddpwdclemndvds  11776  ctiunctlemudc  11877  ctiunctlemf  11878  ctiunctlemfo  11879  ctiunct  11880  cnmpt11  12379  cnmpt1t  12381  cnmpt21  12387  cnmpt2t  12389  cnmptcom  12394  imasnopn  12395  fsumcncntop  12652  ellimc3apf  12725  ellimc3ap  12726  limcmpted  12728  elabf1  12915  elabf2  12916  elabg2  12919  bj-omssind  13060  bj-bdfindisg  13073  bj-nntrans  13076  bj-nnelirr  13078  bj-omtrans  13081  setindis  13092  bdsetindis  13094  bj-nn0sucALT  13103  bj-findis  13104  bj-findisg  13105  strcollnfALT  13111  isomninnlem  13152  trilpolemeq1  13160
  Copyright terms: Public domain W3C validator