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

Theorem nfcv 2421
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
Dummy variable  y is distinct from all other variables.

Proof of Theorem nfcv
StepHypRef Expression
1 nfv 1606 . 2  |-  F/ x  y  e.  A
21nfci 2411 1  |-  F/_ x A
Colors of variables: wff set class
Syntax hints:    e. wcel 1685   F/_wnfc 2408
This theorem is referenced by:  nfcvd  2422  nfel  2429  nfeq1  2430  nfel1  2431  nfeq2  2432  nfel2  2433  nfcvf  2443  r2al  2582  r2ex  2583  nfra2  2599  r19.12  2658  ralcom  2702  rexcom  2703  raleq  2738  rexeq  2739  reueq1  2740  rmoeq1  2741  cbvral  2762  cbvrex  2763  rabeq  2784  cbvrabv  2789  vtoclg  2845  vtocl2g  2849  vtoclga  2851  vtocl2ga  2853  vtocl3ga  2855  spcimdv  2867  spcgv  2870  spcegv  2871  rspct  2879  rspc  2880  rspce  2881  rspc2  2891  ceqsexg  2901  elabgt  2913  elabf  2915  elabg  2917  elab3g  2922  elrab  2925  mob  2949  2rmorex  2971  nfsbc1v  3012  elrabsf  3031  sbcralt  3065  sbcralg  3067  sbcrexg  3068  sbcreug  3069  cbvcsbv  3088  csbexg  3093  csbconstg  3097  nfcsb1v  3115  csbnestg  3133  cbvralcsf  3145  cbvreucsf  3147  cbvrabcsf  3148  cbvralv2  3149  cbvrexv2  3150  n0f  3465  n0  3466  raaan  3563  nfpw  3638  nfop  3814  cbviunv  3943  cbviinv  3944  ssiun2s  3948  iunab  3950  ssiinf  3953  ssiin  3954  iinab  3965  cbvdisjv  4006  disjors  4011  disji2  4012  disjprg  4021  disjxiun  4022  disjxun  4023  cbvmptv  4113  triun  4128  zfrep3cl  4140  moop2  4261  euotd  4267  opelopabf  4289  nfpo  4319  nfso  4320  pofun  4330  nffr  4367  nfse  4368  eusvnf  4529  reusv2lem4  4538  reusv2  4540  reusv6OLD  4545  rabxfrd  4555  onminesb  4589  onminsb  4590  tfis  4645  tfisi  4649  opeliunxp  4740  nfrel  4774  opeliunxp2  4824  ralxpf  4830  nfco  4849  nfcnv  4860  dfdmf  4873  dfrnf  4917  nfdm  4920  nfres  4957  dffun6f  5236  dffun6  5237  nffun  5244  nffvmpt1  5494  dffn5f  5539  funfv2f  5550  fvmpts  5565  fvmpt2i  5569  fvmptss  5571  fvmptex  5572  fvmptdv  5574  fvmptt  5577  fvmptnf  5579  fvmptn  5580  eqfnfv2f  5588  ralrnmpt  5631  f1ompt  5644  ffnfvf  5648  fmptco  5653  fmptcof  5654  fmptcos  5655  zfrep6  5710  abrexex2g  5730  funiunfvf  5737  abrexex2  5742  dff13f  5746  f1mpt  5747  fliftfuns  5775  nfiso  5783  mpt2eq123  5869  cbvmpt2x  5886  cbvmpt2  5887  cbvmpt2v  5888  ovmpt2s  5933  ov2gf  5934  ovmpt2dxf  5935  ovmpt2dx  5936  ovmpt2dv  5942  ovmpt2dv2  5943  ov3  5946  nfof  6045  nfofr  6046  offval2  6057  ofrfval2  6058  dfopab2  6136  dfoprab3s  6137  mpt2mptsx  6149  dmmpt2ssx  6151  fmpt2x  6152  ovmptss  6162  fmpt2co  6164  dfmpt2  6171  nftpos  6231  tposoprab  6232  fvopab5  6283  opabiota  6287  nfriota1  6308  csbriotag  6313  riota2  6323  riotaxfrd  6332  riotasvd  6343  riotasvdOLD  6344  riotasv2d  6345  riotasv2dOLD  6346  riotasv2s  6347  riotasv3dOLD  6350  nfrecs  6386  nfrdg  6423  rdgsucmpt2  6439  rdgsucmpt  6440  frsucmpt  6446  frsucmptn  6447  frsucmpt2  6448  oawordeulem  6548  nnawordex  6631  eqerlem  6688  qliftfuns  6741  cbvixpv  6830  nfixp  6831  nfixp1  6832  ixpf  6834  mptelixpg  6849  dom2lem  6897  xpcomco  6948  xpf1o  7019  mapxpen  7023  ac6sfi  7097  iunfi  7140  indexfi  7159  dffi3  7180  nfoi  7225  ixpiunwdom  7301  cnfcomlem  7398  r1val1  7454  rankidb  7468  rankval4  7535  scottex  7551  scottexs  7553  scott0s  7554  cp  7557  tskwe  7579  cardmin2  7627  fseqenlem1  7647  dfac8clem  7655  acni2  7669  cardaleph  7712  hsmexlem2  8049  axcc2  8059  ac6num  8102  ac6c4  8104  axdclem  8142  iundom2g  8158  uniimadomf  8163  cardmin  8182  pwfseqlem2  8277  pwfseqlem4a  8279  pwfseqlem4  8280  inar1  8393  lble  9702  nnwof  10281  nnwos  10282  fzrevral  10861  nfseq  11051  nfwrd  11421  rlim2  11965  ello1mpt  11990  rlimcld2  12047  o1compt  12056  sumeq1  12157  nfsum1  12158  nfsum  12159  sumeq2w  12160  cbvsum  12163  cbvsumv  12164  cbvsumi  12165  sumfc  12177  summolem2a  12183  zsum  12186  fsum  12188  fsumf1o  12191  sumss  12192  sumss2  12194  fsumcvg2  12195  fsumadd  12206  sumsn  12208  sumsns  12210  isummulc2  12220  fsum2dlem  12228  fsumcnv  12231  fsumcom2  12232  fsumshftm  12238  fsum0diag2  12240  fsummulc2  12241  fsum00  12251  fsumrelem  12260  fsumrlim  12264  fsumo1  12265  o1fsum  12266  fsumiun  12274  isumshft  12293  ruclem1  12504  prmind2  12764  iserodd  12883  pcmpt  12935  pcmptdvds  12937  prdsbas3  13375  prdsdsval2  13378  mreiincl  13493  invfuc  13843  yonedalem4b  14045  odval  14844  gsum2d2lem  15219  gsum2d2  15220  gsumcom2  15221  prdsgsum  15224  dprdwd  15241  dprd2d2  15274  gsumdixp  15387  lss1d  15715  psrass1lem  16118  evlslem4  16240  fiuncmp  17126  iuncon  17149  2ndcdisj  17177  elptr2  17264  ptbasfi  17271  ptunimpt  17285  ptcldmpt  17303  ptclsg  17304  txcnp  17309  ptcnplem  17310  ptcnp  17311  cnmpt11  17352  cnmpt1t  17354  cnmpt21  17360  cnmpt2t  17362  cnmptcom  17367  cnmptk2  17375  cnmpt2k  17377  xkocnv  17500  elmptrab  17517  flfcnp2  17697  ptcmpg  17746  prdsdsf  17926  prdsxmet  17928  fsumcn  18369  fsum2cn  18370  ovolfiniun  18855  ovoliunlem3  18858  ovoliun  18859  ovoliun2  18860  ovoliunnul  18861  finiunmbl  18896  volfiniun  18899  iundisj  18900  iundisj2  18901  iunmbl  18905  voliun  18906  iunmbl2  18909  mbfeqalem  18992  mbfpos  19001  mbfposr  19002  mbfposb  19003  mbfsup  19014  mbfinf  19015  mbflim  19018  i1fposd  19057  itg1climres  19064  itg2splitlem  19098  itg2split  19099  itg2cnlem1  19111  isibl  19115  isibl2  19116  dfitg  19119  itgeq1  19122  nfitg1  19123  nfitg  19124  cbvitg  19125  cbvitgv  19126  itgmpt  19132  itgeqa  19163  itgss3  19164  itgfsum  19176  itgabs  19184  itggt0  19191  itgcn  19192  cbvditgv  19200  limcmpt  19228  limciun  19239  dvmptfsum  19317  dvlipcn  19336  lhop2  19357  dvfsumle  19363  dvfsumabs  19365  dvfsumlem1  19368  dvfsumlem2  19369  dvfsumlem4  19371  dvfsumrlim  19373  dvfsum2  19376  itgparts  19389  itgsubstlem  19390  itgsubst  19391  mpfrcl  19397  elplyd  19579  coeeq2  19619  dgrle  19620  ulmss  19769  itgulm2  19780  leibpi  20233  rlimcnp  20255  rlimcnp2  20256  o1cxp  20264  fsumdvdscom  20420  fsumdvdsmul  20430  fsumvma  20447  lgseisenlem2  20584  dchrisumlema  20632  dchrisumlem2  20634  dchrisumlem3  20635  cnlnadjlem5  22644  chirred  22968  ifeqeqx  23027  abrexss  23034  dfimafnf  23035  ballotlemelo  23040  ballotleme  23049  ballotlemi  23053  ballotlemsval  23061  ballotlemsv  23062  ballotlemrval  23070  ballotlemrinv  23086  cvmcov  23199  cvmliftphtlem  23253  relexpsucr  23431  dedekind  23486  dedekindle  23487  setinds  23536  dfon2lem3  23543  tfisg  23606  wfisg  23611  trpredlem1  23632  trpredtr  23635  trpredmintr  23636  trpred0  23641  trpredrec  23643  frinsg  23647  sltval2  23711  axfelem5  23752  bpolyval  24192  prodeq3ii  24708  nfprod1  24710  nfprod  24711  prodeqfv  24718  fprodserf  24721  fprod1s  24725  fprodp1s  24727  fprodadd  24752  fprodneg  24778  fprodsub  24779  trooo  24794  rltrooo  24815  intopcoaconb  24940  imonclem  25213  cmpmon  25215  iepiclem  25223  sgplpte21a  25533  finminlem  25631  indexa  25812  indexdom  25813  filbcmb  25832  sdclem2  25852  sdclem1  25853  fdc1  25856  totbndbnd  25913  heibor1  25934  elrfirn2  26171  ofmpteq  26197  mzpsubst  26226  eq0rabdioph  26256  sbccomieg  26270  rexrabdioph  26275  rexfrabdioph  26276  rabdiophlem2  26283  elnn0rabdioph  26284  dvdsrabdioph  26291  rabrenfdioph  26297  fphpd  26299  monotuz  26426  monotoddzz  26428  oddcomabszz  26429  setindtrs  26518  wdom2d2  26528  fnwe2val  26546  fnwe2lem1  26547  aomclem6  26556  aomclem8  26559  flcidc  26779  mamufval  26843  compab  27044  evth2f  27086  elunif  27087  fvelrnbf  27089  rfcnpre1  27090  fsumcnf  27092  sumsnd  27097  evthf  27098  refsumcn  27101  rfcnpre2  27102  rfcnpre3  27104  rfcnpre4  27105  rfcnnnub  27107  refsum2cnlem1  27108  refsum2cn  27109  fmul01  27110  fmuldfeqlem1  27112  fmuldfeq  27113  fmul01lt1lem1  27114  fmul01lt1lem2  27115  fmul01lt1  27116  cncfmptss  27117  mulc1cncfg  27121  infrglb  27122  expcnfg  27126  climmulf  27130  climexp  27131  climsuse  27134  climrecf  27135  climinff  27137  dvcosre  27141  itgsin0pilem1  27144  ibliccsinexp  27145  itgsinexplem1  27148  itgsinexp  27149  stoweidlem3  27152  stoweidlem8  27157  stoweidlem14  27163  stoweidlem16  27165  stoweidlem18  27167  stoweidlem19  27168  stoweidlem21  27170  stoweidlem22  27171  stoweidlem23  27172  stoweidlem26  27175  stoweidlem27  27176  stoweidlem28  27177  stoweidlem29  27178  stoweidlem30  27179  stoweidlem31  27180  stoweidlem32  27181  stoweidlem34  27183  stoweidlem35  27184  stoweidlem36  27185  stoweidlem41  27190  stoweidlem42  27191  stoweidlem43  27192  stoweidlem44  27193  stoweidlem45  27194  stoweidlem46  27195  stoweidlem47  27196  stoweidlem48  27197  stoweidlem49  27198  stoweidlem51  27200  stoweidlem52  27201  stoweidlem53  27202  stoweidlem54  27203  stoweidlem55  27204  stoweidlem56  27205  stoweidlem57  27206  stoweidlem58  27207  stoweidlem59  27208  stoweidlem60  27209  stoweidlem62  27211  stowei  27213  wallispilem5  27218  wallispi  27219  stirlinglem2  27224  stirlinglem3  27225  stirlinglem4  27226  stirlinglem5  27227  stirlinglem8  27230  stirlinglem11  27233  stirlinglem12  27234  stirlinglem13  27235  stirlinglem14  27236  stirlinglem15  27237  stirling  27238  cbvral2  27330  cbvrex2  27331  raaan2  27333  2reurex  27339  2reu3  27346  2reu7  27349  2reu8  27350  nfafv  27379  bnj23  28012  bnj1366  28130  bnj1379  28131  bnj1400  28136  bnj1534  28153  bnj1542  28157  bnj607  28216  bnj873  28224  bnj958  28240  bnj1000  28241  bnj981  28250  bnj1014  28260  bnj1123  28284  bnj1204  28310  bnj1388  28331  bnj1398  28332  bnj1408  28334  bnj1445  28342  bnj1446  28343  bnj1447  28344  bnj1448  28345  bnj1449  28346  bnj1466  28351  bnj1467  28352  bnj1463  28353  bnj1312  28356  bnj1498  28359  bnj1519  28363  bnj1520  28364  bnj1525  28367  bnj1529  28368  riotaocN  28667  cdleme26ee  29817  cdleme31sn1  29838  cdleme31se2  29840  cdlemefrs29bpre0  29853  cdlemefs32sn1aw  29871  cdleme43fsv1snlem  29877  cdleme41sn3a  29890  cdleme32d  29901  cdleme32f  29903  cdleme40m  29924  cdleme40n  29925  cdleme42b  29935  ltrniotaval  30038  cdlemksv2  30304  cdlemkuv2  30324  cdlemk36  30370  cdlemk38  30372  cdlemkid  30393  cdlemk19x  30400  cdlemk11t  30403  dihglblem5  30756  hlhilset  31395
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-17 1604
This theorem depends on definitions:  df-bi 179  df-nf 1533  df-nfc 2410
  Copyright terms: Public domain W3C validator