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

Theorem nfcv 2319
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 1528 . 2 𝑥 𝑦𝐴
21nfci 2309 1 𝑥𝐴
Colors of variables: wff set class
Syntax hints:  wcel 2148  wnfc 2306
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1449  ax-17 1526
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-nfc 2308
This theorem is referenced by:  nfcvd  2320  nfel  2328  nfeq1  2329  nfel1  2330  nfeq2  2331  nfel2  2332  nfcvf  2342  r2al  2496  r2ex  2497  nfraldxy  2510  nfrexdxy  2511  nfra2xy  2519  r19.12  2583  ralcom  2640  rexcom  2641  nfreudxy  2650  raleq  2672  rexeq  2673  reueq1  2674  rmoeq1  2675  cbvralw  2698  cbvral  2699  cbvrex  2700  rabeq  2729  rabeqi  2730  cbvrabv  2736  vtoclg  2797  vtocl2g  2801  vtoclga  2803  vtocl2ga  2805  vtocl3ga  2807  spcimdv  2821  spcimedv  2823  spcgv  2824  spcegv  2825  rspct  2834  rspc  2835  rspce  2836  rspc2  2852  ceqsexg  2865  elabgt  2878  elabf  2880  elabg  2883  elab3g  2888  elrab  2893  mob  2919  nfsbc1v  2981  elrabsf  3001  sbcralt  3039  sbcrext  3040  sbcralg  3041  sbcrex  3042  sbcreug  3043  cbvcsbv  3063  csbconstg  3071  nfcsb1v  3090  csbie  3102  csbnestg  3111  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  cbvralv2  3123  cbvrexv2  3124  dfss4st  3368  n0rf  3435  n0r  3436  eq0  3441  raaanlem  3528  nfpw  3587  cbviunv  3923  cbviinv  3924  ssiun2s  3928  iunab  3930  ssiinf  3933  ssiin  3934  iinab  3945  cbvdisjv  3988  nfdisjv  3989  disjnims  3992  disji2  3993  cbvmptv  4096  triun  4111  csbexga  4128  repizf2  4159  moop2  4248  euotd  4251  opelopabf  4271  nfpo  4298  nfso  4299  pofun  4309  nfse  4338  nffrfor  4345  nffr  4346  frind  4349  nfwe  4352  eusvnf  4450  rabxfrd  4466  tfis  4579  tfisi  4583  opeliunxp  4678  nfrel  4708  opeliunxp2  4763  ralxpf  4769  rexxpf  4770  nfco  4788  nfcnv  4802  dfdmf  4816  dfrnf  4864  nfdm  4867  nfres  4905  resmptf  4953  nfiotadw  5177  dffun6f  5225  dffun6  5226  dffun4f  5228  nffun  5235  funimaexglem  5295  nffv  5521  nffvmpt1  5522  dffn5imf  5567  funfvdm2f  5577  fvmptss2  5587  fvmpts  5590  fvmpt2  5595  fvmptssdm  5596  mptfvex  5597  fvmptdv  5600  fvmptd3  5605  elfvmptrab1  5606  eqfnfv2f  5613  ralrnmpt  5654  rexrnmpt  5655  f1ompt  5663  ffnfvf  5671  fmptco  5678  fmptcof  5679  fmptcos  5680  funiunfvdmf  5759  dff13f  5765  f1mpt  5766  fliftfuns  5793  nfiso  5801  nfriotadxy  5833  csbriotag  5837  riota2  5847  mpoeq123  5928  cbvmpox  5947  cbvmpo  5948  cbvmpov  5949  ovmpos  5992  ov2gf  5993  ovmpodxf  5994  ovmpodx  5995  ovmpodv  6001  ovmpodv2  6002  ovi3  6005  nfof  6082  nfofr  6083  offval2  6092  ofrfval2  6093  abrexex2g  6115  abrexex2  6119  dfopab2  6184  dfoprab3s  6185  mpomptsx  6192  dmmpossx  6194  fmpox  6195  mpofvex  6198  fnmpoovd  6210  fmpoco  6211  dfmpo  6218  f1od2  6230  disjxp1  6231  mpoxopoveq  6235  mpoxopovel  6236  nftpos  6274  tposoprab  6275  nfrecs  6302  nffrec  6391  eqerlem  6560  qliftfuns  6613  cbvixpv  6710  nfixpxy  6711  nfixp1  6712  ixpf  6714  mptelixpg  6728  dom2lem  6766  xpcomco  6820  xpf1o  6838  mapxpen  6842  ac6sfi  6892  nfsup  6985  nfdju  7035  exmidomni  7134  ismkvnex  7147  cc2  7254  cc4f  7256  cc4  7257  caucvgprprlemaddq  7695  caucvgsrlemgt1  7782  axpre-suploclemres  7888  lble  8890  supinfneg  9581  infsupneg  9582  fzrevral  10088  nfseq  10438  seq3f1olemstep  10484  seq3f1olemp  10485  fimaxre2  11216  nfsum1  11345  nfsum  11346  cbvsumv  11350  cbvsumi  11351  sumfct  11363  sumrbdclem  11366  summodclem2a  11370  zsumdc  11373  fsum3  11376  isumss  11380  isumss2  11382  fsum3cvg2  11383  fsumzcl2  11394  fsumadd  11395  fsumsplitf  11397  sumsnf  11398  sumsn  11400  sumsns  11404  fsumsplitsnun  11408  fsum2dlemstep  11423  fisumcom2  11427  fsumshftm  11434  fsum00  11451  fsumrelem  11460  fsumiun  11466  mertenslem2  11525  prodeq1  11542  nfcprod1  11543  nfcprod  11544  cbvprod  11547  cbvprodv  11548  cbvprodi  11549  prodrbdclem  11560  prodmodclem2a  11565  zproddc  11568  fprodseq  11572  fprodntrivap  11573  prodfct  11576  prodssdc  11578  prodsnf  11581  prodsn  11582  fprodm1s  11590  fprodp1s  11591  prodsns  11592  fprodcllemf  11602  fprodconst  11609  fprodap0  11610  fprod2dlemstep  11611  fprodcom2fi  11615  fprodrec  11618  fproddivapf  11620  fprodsplitf  11621  fprodap0f  11625  fprodle  11629  zsupcllemstep  11926  infssuzex  11930  infssuzcldc  11932  bezoutlemmain  11979  bezout  11992  nnwofdc  12019  nnwosdc  12020  prmind2  12100  oddpwdclemdvds  12150  oddpwdclemndvds  12151  pcmpt  12321  pcmptdvds  12323  ctiunctlemudc  12418  ctiunctlemf  12419  ctiunctlemfo  12420  ctiunct  12421  ctiunctal  12422  cnmpt11  13443  cnmpt1t  13445  cnmpt21  13451  cnmpt2t  13453  cnmptcom  13458  imasnopn  13459  fsumcncntop  13716  ellimc3apf  13789  ellimc3ap  13790  limcmpted  13792  elabf1  14182  elabf2  14183  elabg2  14186  bj-omssind  14336  bj-bdfindisg  14349  bj-nntrans  14352  bj-nnelirr  14354  bj-omtrans  14357  setindis  14368  bdsetindis  14370  bj-nn0sucALT  14379  bj-findis  14380  bj-findisg  14381  strcollnfALT  14387  isomninnlem  14427  trilpolemeq1  14437  trirec0  14441  iswomninnlem  14446  ismkvnnlem  14449  nconstwlpolemgt0  14460
  Copyright terms: Public domain W3C validator