MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfcv Structured version   Unicode version

Theorem nfcv 2572
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 1629 . 2  |-  F/ x  y  e.  A
21nfci 2562 1  |-  F/_ x A
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   F/_wnfc 2559
This theorem is referenced by:  nfcvd  2573  nfel  2580  nfeq1  2581  nfel1  2582  nfeq2  2583  nfel2  2584  nfcvf  2594  r2al  2742  r2ex  2743  nfra2  2760  r19.12  2819  ralcom  2868  rexcom  2869  raleq  2904  rexeq  2905  reueq1  2906  rmoeq1  2907  cbvral  2928  cbvrex  2929  rabeq  2950  cbvrabv  2955  vtoclg  3011  vtocl2g  3015  vtoclga  3017  vtocl2ga  3019  vtocl3ga  3021  spcimdv  3033  spcgv  3036  spcegv  3037  rspct  3045  rspc  3046  rspce  3047  rspc2  3057  ceqsexg  3067  elabgt  3079  elabf  3081  elabg  3083  elab3g  3088  elrab  3092  mob  3116  2rmorex  3138  nfsbc1v  3180  elrabsf  3199  sbcralt  3233  sbcralg  3235  sbcrexg  3236  sbcreug  3237  cbvcsbv  3256  csbexg  3261  csbconstg  3265  nfcsb1v  3283  csbnestg  3301  cbvralcsf  3311  cbvreucsf  3313  cbvrabcsf  3314  cbvralv2  3315  cbvrexv2  3316  n0f  3636  n0  3637  raaan  3735  nfpw  3810  nfop  4000  cbviunv  4130  cbviinv  4131  ssiun2s  4135  iunab  4137  ssiinf  4140  ssiin  4141  iinab  4152  cbvdisjv  4193  disjors  4198  disji2  4199  disjprg  4208  disjxiun  4209  disjxun  4210  cbvmptv  4300  triun  4315  zfrep3cl  4327  moop2  4451  euotd  4457  opelopabf  4479  nfpo  4508  nfso  4509  pofun  4519  nffr  4556  nfse  4557  eusvnf  4718  reusv2lem4  4727  reusv2  4729  reusv6OLD  4734  rabxfrd  4744  onminesb  4778  onminsb  4779  tfis  4834  tfisi  4838  opeliunxp  4929  nfrel  4962  opeliunxp2  5013  ralxpf  5019  nfco  5038  nfcnv  5051  dfdmf  5064  dfrnf  5108  nfdm  5111  nfres  5148  dffun6f  5468  dffun6  5469  nffun  5476  nffv  5735  nffvmpt1  5736  dffn5f  5781  funfv2f  5792  fvmpts  5807  fvmpt2i  5811  fvmptss  5813  fvmptex  5815  fvmptdv  5817  fvmptnf  5822  fvmptn  5823  eqfnfv2f  5831  ralrnmpt  5878  f1ompt  5891  ffnfvf  5895  fmptco  5901  fmptcof  5902  fmptcos  5903  zfrep6  5968  abrexex2g  5988  funiunfvf  5996  abrexex2  6001  dff13f  6006  f1mpt  6007  fliftfuns  6036  nfiso  6044  mpt2eq123  6133  cbvmpt2x  6150  cbvmpt2  6151  cbvmpt2v  6152  ovmpt2s  6197  ov2gf  6198  ovmpt2dxf  6199  ovmpt2dx  6200  ovmpt2dv  6206  ovmpt2dv2  6207  ov3  6210  nfof  6310  nfofr  6311  offval2  6322  ofrfval2  6323  dfopab2  6401  dfoprab3s  6402  mpt2mptsx  6414  dmmpt2ssx  6416  fmpt2x  6417  ovmptss  6428  fmpt2co  6430  dfmpt2  6437  mpt2xopoveq  6470  mpt2xopovel  6471  nftpos  6514  tposoprab  6515  fvopab5  6534  nfriota1  6557  csbriotag  6562  riota2  6572  riotaxfrd  6581  riotasvd  6592  riotasvdOLD  6593  riotasv2d  6594  riotasv2dOLD  6595  riotasv2s  6596  riotasv3dOLD  6599  nfrecs  6635  nfrdg  6672  rdgsucmpt2  6688  rdgsucmpt  6689  frsucmpt  6695  frsucmptn  6696  frsucmpt2  6697  oawordeulem  6797  nnawordex  6880  eqerlem  6937  qliftfuns  6991  cbvixpv  7080  nfixp  7081  nfixp1  7082  ixpf  7084  mptelixpg  7099  dom2lem  7147  xpcomco  7198  xpf1o  7269  mapxpen  7273  ac6sfi  7351  iunfi  7394  indexfi  7414  dffi3  7436  nfoi  7483  ixpiunwdom  7559  cnfcomlem  7656  r1val1  7712  rankidb  7726  rankval4  7793  scottex  7809  scottexs  7811  scott0s  7812  cp  7815  tskwe  7837  cardmin2  7885  fseqenlem1  7905  dfac8clem  7913  cardaleph  7970  hsmexlem2  8307  axcc2  8317  ac6num  8359  ac6c4  8361  axdclem  8399  iundom2g  8415  uniimadomf  8420  cardmin  8439  pwfseqlem2  8534  pwfseqlem4a  8536  pwfseqlem4  8537  inar1  8650  lble  9960  nnwof  10543  nnwos  10544  fzrevral  11131  nfseq  11333  seqof2  11381  nfwrd  11740  rlim2  12290  ello1mpt  12315  rlimcld2  12372  o1compt  12381  sumeq1  12483  nfsum1  12484  nfsum  12485  sumeq2w  12486  cbvsum  12489  cbvsumv  12490  cbvsumi  12491  sumfc  12503  summolem2a  12509  zsum  12512  fsum  12514  sumss  12518  sumss2  12520  fsumcvg2  12521  fsumadd  12532  sumsn  12534  sumsns  12536  fsum2dlem  12554  fsumcnv  12557  fsumcom2  12558  fsumshftm  12564  fsum0diag2  12566  fsummulc2  12567  fsum00  12577  fsumrelem  12586  fsumrlim  12590  fsumo1  12591  o1fsum  12592  fsumiun  12600  ruclem1  12830  prmind2  13090  pcmpt  13261  pcmptdvds  13263  prdsbas3  13703  prdsdsval2  13706  mreiincl  13821  invfuc  14171  yonedalem4b  14373  odval  15172  gsum2d2lem  15547  gsum2d2  15548  gsumcom2  15549  prdsgsum  15552  dprd2d2  15602  gsumdixp  15715  lss1d  16039  psrass1lem  16442  evlslem4  16564  neiptopnei  17196  fiuncmp  17467  iuncon  17491  2ndcdisj  17519  elptr2  17606  ptbasfi  17613  ptunimpt  17627  ptcldmpt  17646  ptclsg  17647  ptcnplem  17653  ptcnp  17654  cnmpt11  17695  cnmpt1t  17697  cnmpt21  17703  cnmpt2t  17705  cnmptcom  17710  cnmptk2  17718  cnmpt2k  17720  imasnopn  17722  imasncld  17723  imasncls  17724  xkocnv  17846  elmptrab  17859  flfcnp2  18039  ptcmpg  18088  cnextfvval  18096  fmucnd  18322  prdsdsf  18397  prdsxmet  18399  cfilucfilOLD  18599  cfilucfil  18600  blval2  18605  restmetu  18617  fsumcn  18900  fsum2cn  18901  ovolfiniun  19397  ovoliunlem3  19400  ovoliun  19401  ovoliun2  19402  ovoliunnul  19403  finiunmbl  19438  volfiniun  19441  iundisj  19442  iundisj2  19443  iunmbl  19447  voliun  19448  iunmbl2  19451  mbfpos  19543  mbfposr  19544  mbfposb  19545  mbfsup  19556  mbfinf  19557  mbflim  19560  i1fposd  19599  itg1climres  19606  itg2splitlem  19640  itg2split  19641  itg2cnlem1  19653  isibl  19657  isibl2  19658  dfitg  19661  itgeq1  19664  nfitg1  19665  nfitg  19666  cbvitg  19667  cbvitgv  19668  itgmpt  19674  itgss3  19706  itgfsum  19718  itgabs  19726  itggt0  19733  itgcn  19734  cbvditgv  19742  limcmpt  19770  limciun  19781  dvmptfsum  19859  dvlipcn  19878  lhop2  19899  dvfsumle  19905  dvfsumabs  19907  dvfsumlem1  19910  dvfsumlem2  19911  dvfsumlem4  19913  dvfsumrlim  19915  dvfsum2  19918  itgparts  19931  itgsubstlem  19932  itgsubst  19933  mpfrcl  19939  elplyd  20121  coeeq2  20161  dgrle  20162  ulmss  20313  itgulm2  20325  leibpi  20782  rlimcnp  20804  rlimcnp2  20805  o1cxp  20813  fsumdvdscom  20970  fsumdvdsmul  20980  fsumvma  20997  lgseisenlem2  21134  dchrisumlema  21182  dchrisumlem2  21184  dchrisumlem3  21185  cnlnadjlem5  23574  chirred  23898  ralcom4f  23965  rexcom4f  23966  rmo4fOLD  23983  disji2f  24019  disjorsf  24022  disjif2  24023  disjabrex  24024  disjabrexf  24025  disjxpin  24028  iundisjf  24029  iundisj2f  24030  dfrel4  24034  dfimafnf  24043  suppss2f  24049  fmptdF  24069  resmptf  24071  fvmpt2f  24072  feqmptdf  24075  fmptcof2  24076  fcomptf  24077  offval2f  24080  ofpreima  24081  funcnvmptOLD  24082  funcnvmpt  24083  funcnv5mpt  24084  funcnv4mpt  24085  xrofsup  24126  iundisjfi  24152  iundisj2fi  24153  iundisjcnt  24154  iundisj2cnt  24155  gsumconstf  24222  xrge0tmd  24332  qqhval2  24366  esumcl  24427  nfesum1  24437  cbvesumv  24439  esumid  24440  esumval  24441  esumel  24442  esumnul  24443  esumsplit  24447  esumadd  24448  esumle  24449  esummono  24450  gsumesum  24451  esumlub  24452  esumaddf  24453  esumpr  24457  esumfzf  24459  esumfsup  24460  esumss  24462  esumpinfval  24463  esumpfinvalf  24466  esumpinfsum  24467  esumpcvgval  24468  esumpmono  24469  esumcocn  24470  esummulc1  24471  esummulc2  24472  esumdivc  24473  esumcvg  24476  sigaclcu2  24503  measvunilem  24566  measvunilem0  24567  measvuni  24568  measiuns  24571  measiun  24572  meascnbl  24573  voliune  24585  volfiniune  24586  volmeas  24587  imambfm  24612  sibfof  24654  lgamgulmlem2  24814  lgamgulmlem6  24818  lgamgulm2  24820  cvmcov  24950  relexpsucr  25130  prodeq1  25235  nfcprod1  25236  nfcprod  25237  prodeq2w  25238  cbvprod  25241  cbvprodv  25242  cbvprodi  25243  prodmolem2a  25260  zprod  25263  fprod  25267  fprodntriv  25268  prodfc  25271  prodss  25273  fprodmul  25284  fproddiv  25285  prodsn  25286  fprodm1s  25293  fprodp1s  25294  prodsns  25295  fprodefsum  25298  fprodn0  25303  fprod2dlem  25304  fprodcnv  25307  fprodcom2  25308  setinds  25405  dfon2lem3  25412  tfisg  25479  wfisg  25484  trpredlem1  25505  trpredtr  25508  trpredmintr  25509  trpred0  25514  trpredrec  25516  frinsg  25520  nfwrecs  25533  nfwlim  25573  sltval2  25611  nobndlem5  25651  bpolyval  26095  mbfposadd  26254  itgabsnc  26274  itggt0cn  26277  ftc1cnnclem  26278  ftc1anclem5  26284  ftc2nc  26289  finminlem  26321  indexa  26435  indexdom  26436  filbcmb  26442  sdclem2  26446  sdclem1  26447  fdc1  26450  totbndbnd  26498  heibor1  26519  elrfirn2  26750  ofmpteq  26776  mzpsubst  26805  eq0rabdioph  26835  sbccomieg  26849  rexrabdioph  26854  rexfrabdioph  26855  rabdiophlem2  26862  elnn0rabdioph  26863  dvdsrabdioph  26870  rabrenfdioph  26875  fphpd  26877  monotuz  27004  monotoddzz  27006  oddcomabszz  27007  setindtrs  27096  wdom2d2  27106  fnwe2val  27124  fnwe2lem1  27125  aomclem6  27134  aomclem8  27136  mamufval  27420  compab  27620  evth2f  27662  elunif  27663  fvelrnbf  27665  rfcnpre1  27666  fsumcnf  27668  sumsnd  27673  evthf  27674  refsumcn  27677  rfcnpre2  27678  rfcnpre3  27680  rfcnpre4  27681  rfcnnnub  27683  refsum2cnlem1  27684  refsum2cn  27685  fmul01  27686  fmuldfeqlem1  27688  fmuldfeq  27689  fmul01lt1lem1  27690  fmul01lt1lem2  27691  fmul01lt1  27692  cncfmptss  27693  mulc1cncfg  27697  infrglb  27698  expcnfg  27702  climmulf  27706  climexp  27707  climsuse  27710  climrecf  27711  climinff  27713  dvcosre  27717  itgsin0pilem1  27720  ibliccsinexp  27721  itgsinexplem1  27724  itgsinexp  27725  stoweidlem3  27728  stoweidlem14  27739  stoweidlem16  27741  stoweidlem18  27743  stoweidlem21  27746  stoweidlem23  27748  stoweidlem26  27751  stoweidlem27  27752  stoweidlem28  27753  stoweidlem29  27754  stoweidlem31  27756  stoweidlem34  27759  stoweidlem35  27760  stoweidlem36  27761  stoweidlem41  27766  stoweidlem42  27767  stoweidlem43  27768  stoweidlem46  27771  stoweidlem47  27772  stoweidlem48  27773  stoweidlem51  27776  stoweidlem52  27777  stoweidlem53  27778  stoweidlem54  27779  stoweidlem55  27780  stoweidlem56  27781  stoweidlem57  27782  stoweidlem58  27783  stoweidlem59  27784  stoweidlem60  27785  stoweidlem62  27787  stowei  27789  wallispilem5  27794  stirlinglem4  27802  stirlinglem5  27803  stirlinglem11  27809  stirlinglem12  27810  stirlinglem13  27811  stirlinglem14  27812  stirlinglem15  27813  stirling  27814  cbvral2  27926  cbvrex2  27927  raaan2  27929  2reurex  27935  2reu3  27942  2reu7  27945  2reu8  27946  eu2ndop1stv  27956  nfafv  27976  opelopabgf  28071  oprabv  28085  iunconlem2  29047  bnj23  29083  bnj1366  29201  bnj1400  29207  bnj1534  29224  bnj1542  29228  bnj607  29287  bnj873  29295  bnj958  29311  bnj1000  29312  bnj981  29321  bnj1014  29331  bnj1123  29355  bnj1204  29381  bnj1388  29402  bnj1398  29403  bnj1408  29405  bnj1445  29413  bnj1446  29414  bnj1447  29415  bnj1448  29416  bnj1449  29417  bnj1466  29422  bnj1467  29423  bnj1463  29424  bnj1312  29427  bnj1498  29430  bnj1519  29434  bnj1520  29435  bnj1525  29438  bnj1529  29439  riotaocN  30007  cdleme26ee  31157  cdleme31sn1  31178  cdleme31se2  31180  cdlemefrs29bpre0  31193  cdlemefs32sn1aw  31211  cdleme43fsv1snlem  31217  cdleme41sn3a  31230  cdleme32d  31241  cdleme32f  31243  cdleme40m  31264  cdleme40n  31265  cdleme42b  31275  ltrniotaval  31378  cdlemksv2  31644  cdlemkuv2  31664  cdlemk36  31710  cdlemk38  31712  cdlemkid  31733  cdlemk19x  31740  cdlemk11t  31743  dihglblem5  32096  hlhilset  32735
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-17 1626
This theorem depends on definitions:  df-bi 178  df-nf 1554  df-nfc 2561
  Copyright terms: Public domain W3C validator