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

Theorem nfcv 2282
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 1509 . 2 𝑥 𝑦𝐴
21nfci 2272 1 𝑥𝐴
Colors of variables: wff set class
Syntax hints:  wcel 1481  wnfc 2269
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 1426  ax-17 1507
This theorem depends on definitions:  df-bi 116  df-nf 1438  df-nfc 2271
This theorem is referenced by:  nfcvd  2283  nfel  2291  nfeq1  2292  nfel1  2293  nfeq2  2294  nfel2  2295  nfcvf  2304  r2al  2457  r2ex  2458  nfraldxy  2470  nfrexdxy  2471  nfra2xy  2478  r19.12  2541  ralcom  2597  rexcom  2598  nfreudxy  2607  raleq  2629  rexeq  2630  reueq1  2631  rmoeq1  2632  cbvral  2653  cbvrex  2654  rabeq  2681  rabeqi  2682  cbvrabv  2688  vtoclg  2749  vtocl2g  2753  vtoclga  2755  vtocl2ga  2757  vtocl3ga  2759  spcimdv  2773  spcimedv  2775  spcgv  2776  spcegv  2777  rspct  2786  rspc  2787  rspce  2788  rspc2  2804  ceqsexg  2817  elabgt  2829  elabf  2831  elabg  2834  elab3g  2839  elrab  2844  mob  2870  nfsbc1v  2931  elrabsf  2951  sbcralt  2989  sbcrext  2990  sbcralg  2991  sbcrex  2992  sbcreug  2993  cbvcsbv  3013  csbconstg  3021  nfcsb1v  3040  csbie  3050  csbnestg  3059  cbvralcsf  3067  cbvrexcsf  3068  cbvreucsf  3069  cbvrabcsf  3070  cbvralv2  3071  cbvrexv2  3072  dfss4st  3314  n0rf  3380  n0r  3381  eq0  3386  raaanlem  3473  nfpw  3528  cbviunv  3860  cbviinv  3861  ssiun2s  3865  iunab  3867  ssiinf  3870  ssiin  3871  iinab  3882  cbvdisjv  3925  nfdisjv  3926  disjnims  3929  disji2  3930  cbvmptv  4032  triun  4047  csbexga  4064  repizf2  4094  moop2  4181  euotd  4184  opelopabf  4204  nfpo  4231  nfso  4232  pofun  4242  nfse  4271  nffrfor  4278  nffr  4279  frind  4282  nfwe  4285  eusvnf  4382  rabxfrd  4398  tfis  4505  tfisi  4509  opeliunxp  4602  nfrel  4632  opeliunxp2  4687  ralxpf  4693  rexxpf  4694  nfco  4712  nfcnv  4726  dfdmf  4740  dfrnf  4788  nfdm  4791  nfres  4829  resmptf  4877  nfiotadw  5099  dffun6f  5144  dffun6  5145  dffun4f  5147  nffun  5154  funimaexglem  5214  nffv  5439  nffvmpt1  5440  dffn5imf  5484  funfvdm2f  5494  fvmptss2  5504  fvmpts  5507  fvmpt2  5512  fvmptssdm  5513  mptfvex  5514  fvmptdv  5517  fvmptd3  5522  elfvmptrab1  5523  eqfnfv2f  5530  ralrnmpt  5570  rexrnmpt  5571  f1ompt  5579  ffnfvf  5587  fmptco  5594  fmptcof  5595  fmptcos  5596  funiunfvdmf  5673  dff13f  5679  f1mpt  5680  fliftfuns  5707  nfiso  5715  nfriotadxy  5746  csbriotag  5750  riota2  5760  mpoeq123  5838  cbvmpox  5857  cbvmpo  5858  cbvmpov  5859  ovmpos  5902  ov2gf  5903  ovmpodxf  5904  ovmpodx  5905  ovmpodv  5911  ovmpodv2  5912  ovi3  5915  nfof  5995  nfofr  5996  offval2  6005  ofrfval2  6006  abrexex2g  6026  abrexex2  6030  dfopab2  6095  dfoprab3s  6096  mpomptsx  6103  dmmpossx  6105  fmpox  6106  mpofvex  6109  fnmpoovd  6120  fmpoco  6121  dfmpo  6128  f1od2  6140  disjxp1  6141  mpoxopoveq  6145  mpoxopovel  6146  nftpos  6184  tposoprab  6185  nfrecs  6212  nffrec  6301  eqerlem  6468  qliftfuns  6521  cbvixpv  6618  nfixpxy  6619  nfixp1  6620  ixpf  6622  mptelixpg  6636  dom2lem  6674  xpcomco  6728  xpf1o  6746  mapxpen  6750  ac6sfi  6800  nfsup  6887  nfdju  6935  exmidomni  7022  ismkvnex  7037  cc2  7099  cc4f  7101  cc4  7102  caucvgprprlemaddq  7540  caucvgsrlemgt1  7627  axpre-suploclemres  7733  lble  8729  supinfneg  9417  infsupneg  9418  fzrevral  9916  nfseq  10259  seq3f1olemstep  10305  seq3f1olemp  10306  fimaxre2  11030  nfsum1  11157  nfsum  11158  cbvsumv  11162  cbvsumi  11163  sumfct  11175  sumrbdclem  11178  summodclem2a  11182  zsumdc  11185  fsum3  11188  isumss  11192  isumss2  11194  fsum3cvg2  11195  fsumzcl2  11206  fsumadd  11207  fsumsplitf  11209  sumsnf  11210  sumsn  11212  sumsns  11216  fsumsplitsnun  11220  fsum2dlemstep  11235  fisumcom2  11239  fsumshftm  11246  fsum00  11263  fsumrelem  11272  fsumiun  11278  mertenslem2  11337  prodeq1  11354  nfcprod1  11355  nfcprod  11356  cbvprod  11359  cbvprodv  11360  cbvprodi  11361  prodrbdclem  11372  prodmodclem2a  11377  zproddc  11380  fprodseq  11384  zsupcllemstep  11674  infssuzex  11678  infssuzcldc  11680  bezoutlemmain  11722  bezout  11735  prmind2  11837  oddpwdclemdvds  11884  oddpwdclemndvds  11885  ctiunctlemudc  11986  ctiunctlemf  11987  ctiunctlemfo  11988  ctiunct  11989  ctiunctal  11990  cnmpt11  12491  cnmpt1t  12493  cnmpt21  12499  cnmpt2t  12501  cnmptcom  12506  imasnopn  12507  fsumcncntop  12764  ellimc3apf  12837  ellimc3ap  12838  limcmpted  12840  elabf1  13159  elabf2  13160  elabg2  13163  bj-omssind  13304  bj-bdfindisg  13317  bj-nntrans  13320  bj-nnelirr  13322  bj-omtrans  13325  setindis  13336  bdsetindis  13338  bj-nn0sucALT  13347  bj-findis  13348  bj-findisg  13349  strcollnfALT  13355  isomninnlem  13400  trilpolemeq1  13408  trirec0  13412  iswomninnlem  13417  ismkvnnlem  13419
  Copyright terms: Public domain W3C validator