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

Theorem nfcv 2419
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 1605 . 2  |-  F/ x  y  e.  A
21nfci 2409 1  |-  F/_ x A
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   F/_wnfc 2406
This theorem is referenced by:  nfcvd  2420  nfel  2427  nfeq1  2428  nfel1  2429  nfeq2  2430  nfel2  2431  nfcvf  2441  r2al  2580  r2ex  2581  nfra2  2597  r19.12  2656  ralcom  2700  rexcom  2701  raleq  2736  rexeq  2737  reueq1  2738  rmoeq1  2739  cbvral  2760  cbvrex  2761  rabeq  2782  cbvrabv  2787  vtoclg  2843  vtocl2g  2847  vtoclga  2849  vtocl2ga  2851  vtocl3ga  2853  spcimdv  2865  spcgv  2868  spcegv  2869  rspct  2877  rspc  2878  rspce  2879  rspc2  2889  ceqsexg  2899  elabgt  2911  elabf  2913  elabg  2915  elab3g  2920  elrab  2923  mob  2947  2rmorex  2969  nfsbc1v  3010  elrabsf  3029  sbcralt  3063  sbcralg  3065  sbcrexg  3066  sbcreug  3067  cbvcsbv  3086  csbexg  3091  csbconstg  3095  nfcsb1v  3113  csbnestg  3131  cbvralcsf  3143  cbvreucsf  3145  cbvrabcsf  3146  cbvralv2  3147  cbvrexv2  3148  n0f  3463  n0  3464  raaan  3561  nfpw  3636  nfop  3812  cbviunv  3941  cbviinv  3942  ssiun2s  3946  iunab  3948  ssiinf  3951  ssiin  3952  iinab  3963  cbvdisjv  4004  disjors  4009  disji2  4010  disjprg  4019  disjxiun  4020  disjxun  4021  cbvmptv  4111  triun  4126  zfrep3cl  4138  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  5269  dffun6  5270  nffun  5277  nffv  5532  nffvmpt1  5533  dffn5f  5577  funfv2f  5588  fvmpts  5603  fvmpt2i  5607  fvmptss  5609  fvmptex  5610  fvmptdv  5612  fvmptt  5615  fvmptnf  5617  fvmptn  5618  eqfnfv2f  5626  ralrnmpt  5669  f1ompt  5682  ffnfvf  5686  fmptco  5691  fmptcof  5692  fmptcos  5693  zfrep6  5748  abrexex2g  5768  funiunfvf  5775  abrexex2  5780  dff13f  5784  f1mpt  5785  fliftfuns  5813  nfiso  5821  mpt2eq123  5907  cbvmpt2x  5924  cbvmpt2  5925  cbvmpt2v  5926  ovmpt2s  5971  ov2gf  5972  ovmpt2dxf  5973  ovmpt2dx  5974  ovmpt2dv  5980  ovmpt2dv2  5981  ov3  5984  nfof  6083  nfofr  6084  offval2  6095  ofrfval2  6096  dfopab2  6174  dfoprab3s  6175  mpt2mptsx  6187  dmmpt2ssx  6189  fmpt2x  6190  ovmptss  6200  fmpt2co  6202  dfmpt2  6209  nftpos  6269  tposoprab  6270  fvopab5  6289  opabiota  6293  nfriota1  6312  csbriotag  6317  riota2  6327  riotaxfrd  6336  riotasvd  6347  riotasvdOLD  6348  riotasv2d  6349  riotasv2dOLD  6350  riotasv2s  6351  riotasv3dOLD  6354  nfrecs  6390  nfrdg  6427  rdgsucmpt2  6443  rdgsucmpt  6444  frsucmpt  6450  frsucmptn  6451  frsucmpt2  6452  oawordeulem  6552  nnawordex  6635  eqerlem  6692  qliftfuns  6745  cbvixpv  6834  nfixp  6835  nfixp1  6836  ixpf  6838  mptelixpg  6853  dom2lem  6901  xpcomco  6952  xpf1o  7023  mapxpen  7027  ac6sfi  7101  iunfi  7144  indexfi  7163  dffi3  7184  nfoi  7229  ixpiunwdom  7305  cnfcomlem  7402  r1val1  7458  rankidb  7472  rankval4  7539  scottex  7555  scottexs  7557  scott0s  7558  cp  7561  tskwe  7583  cardmin2  7631  fseqenlem1  7651  dfac8clem  7659  acni2  7673  cardaleph  7716  hsmexlem2  8053  axcc2  8063  ac6num  8106  ac6c4  8108  axdclem  8146  iundom2g  8162  uniimadomf  8167  cardmin  8186  pwfseqlem2  8281  pwfseqlem4a  8283  pwfseqlem4  8284  inar1  8397  lble  9706  nnwof  10285  nnwos  10286  fzrevral  10866  nfseq  11056  nfwrd  11426  rlim2  11970  ello1mpt  11995  rlimcld2  12052  o1compt  12061  sumeq1  12162  nfsum1  12163  nfsum  12164  sumeq2w  12165  cbvsum  12168  cbvsumv  12169  cbvsumi  12170  sumfc  12182  summolem2a  12188  zsum  12191  fsum  12193  fsumf1o  12196  sumss  12197  sumss2  12199  fsumcvg2  12200  fsumadd  12211  sumsn  12213  sumsns  12215  isummulc2  12225  fsum2dlem  12233  fsumcnv  12236  fsumcom2  12237  fsumshftm  12243  fsum0diag2  12245  fsummulc2  12246  fsum00  12256  fsumrelem  12265  fsumrlim  12269  fsumo1  12270  o1fsum  12271  fsumiun  12279  isumshft  12298  ruclem1  12509  prmind2  12769  iserodd  12888  pcmpt  12940  pcmptdvds  12942  prdsbas3  13380  prdsdsval2  13383  mreiincl  13498  invfuc  13848  yonedalem4b  14050  odval  14849  gsum2d2lem  15224  gsum2d2  15225  gsumcom2  15226  prdsgsum  15229  dprdwd  15246  dprd2d2  15279  gsumdixp  15392  lss1d  15720  psrass1lem  16123  evlslem4  16245  fiuncmp  17131  iuncon  17154  2ndcdisj  17182  elptr2  17269  ptbasfi  17276  ptunimpt  17290  ptcldmpt  17308  ptclsg  17309  txcnp  17314  ptcnplem  17315  ptcnp  17316  cnmpt11  17357  cnmpt1t  17359  cnmpt21  17365  cnmpt2t  17367  cnmptcom  17372  cnmptk2  17380  cnmpt2k  17382  xkocnv  17505  elmptrab  17522  flfcnp2  17702  ptcmpg  17751  prdsdsf  17931  prdsxmet  17933  fsumcn  18374  fsum2cn  18375  ovolfiniun  18860  ovoliunlem3  18863  ovoliun  18864  ovoliun2  18865  ovoliunnul  18866  finiunmbl  18901  volfiniun  18904  iundisj  18905  iundisj2  18906  iunmbl  18910  voliun  18911  iunmbl2  18914  mbfeqalem  18997  mbfpos  19006  mbfposr  19007  mbfposb  19008  mbfsup  19019  mbfinf  19020  mbflim  19023  i1fposd  19062  itg1climres  19069  itg2splitlem  19103  itg2split  19104  itg2cnlem1  19116  isibl  19120  isibl2  19121  dfitg  19124  itgeq1  19127  nfitg1  19128  nfitg  19129  cbvitg  19130  cbvitgv  19131  itgmpt  19137  itgeqa  19168  itgss3  19169  itgfsum  19181  itgabs  19189  itggt0  19196  itgcn  19197  cbvditgv  19205  limcmpt  19233  limciun  19244  dvmptfsum  19322  dvlipcn  19341  lhop2  19362  dvfsumle  19368  dvfsumabs  19370  dvfsumlem1  19373  dvfsumlem2  19374  dvfsumlem4  19376  dvfsumrlim  19378  dvfsum2  19381  itgparts  19394  itgsubstlem  19395  itgsubst  19396  mpfrcl  19402  elplyd  19584  coeeq2  19624  dgrle  19625  ulmss  19774  itgulm2  19785  leibpi  20238  rlimcnp  20260  rlimcnp2  20261  o1cxp  20269  fsumdvdscom  20425  fsumdvdsmul  20435  fsumvma  20452  lgseisenlem2  20589  dchrisumlema  20637  dchrisumlem2  20639  dchrisumlem3  20640  cnlnadjlem5  22651  chirred  22975  ifeqeqx  23034  abrexss  23040  dfimafnf  23041  ballotlemelo  23046  ballotleme  23055  ballotlemi  23059  ballotlemsval  23067  ballotlemsv  23068  ballotlemrval  23076  ballotlemrinv  23092  ralcom4f  23133  rexcom4f  23134  clelsb3f  23142  rmo3f  23178  rmo4fOLD  23179  suppss2f  23201  dfrel4  23204  ofrn2  23207  cbvmptf  23220  fmptdF  23221  fmpt3d  23222  resmptf  23223  fvmpt2f  23224  feqmptdf  23228  fmptcof2  23229  fcomptf  23230  offval2f  23233  funcnvmptOLD  23234  funcnvmpt  23235  funcnv5mpt  23236  funcnv4mpt  23237  xrofsup  23255  xrge0mulc1cn  23323  xrge0tmdALT  23327  xrge0tmd  23328  cbvdisjf  23350  disji2f  23354  disjorf  23356  disjorsf  23357  disjif2  23358  disjabrex  23359  disjabrexf  23360  iundisjfi  23363  iundisj2fi  23364  iundisjf  23365  iundisj2f  23366  iundisjcnt  23367  iundisj2cnt  23368  gsumconstf  23381  hashunif  23385  esumcl  23413  cbvesumv  23423  esumid  23424  esumval  23425  esumel  23426  esumnul  23427  esum0  23428  esumsplit  23431  esumadd  23432  esumle  23433  esumaddf  23434  esumcst  23436  esumpr  23438  esumss  23440  esumpinfval  23441  esumpfinval  23443  esumpfinvalf  23444  esumpinfsum  23445  esumpcvgval  23446  esumpmono  23447  esumcocn  23448  esummulc1  23449  esummulc2  23450  esumdivc  23451  esumcvg  23454  sigaclcuni  23479  sigaclcu2  23481  measvunilem  23540  measvunilem0  23541  measvuni  23542  measiuns  23544  measiun  23545  meascnbl  23546  imambfm  23567  dya2iocrrnval  23582  cvmcov  23794  cvmliftphtlem  23848  relexpsucr  24026  dedekind  24082  dedekindle  24083  setinds  24134  dfon2lem3  24141  tfisg  24204  wfisg  24209  trpredlem1  24230  trpredtr  24233  trpredmintr  24234  trpred0  24239  trpredrec  24241  frinsg  24245  sltval2  24310  nobndlem5  24350  bpolyval  24784  prodeq3ii  25308  nfprod1  25310  nfprod  25311  prodeqfv  25318  fprodserf  25321  fprod1s  25325  fprodp1s  25327  fprodadd  25352  fprodneg  25378  fprodsub  25379  trooo  25394  rltrooo  25415  intopcoaconb  25540  imonclem  25813  cmpmon  25815  iepiclem  25823  sgplpte21a  26133  finminlem  26231  indexa  26412  indexdom  26413  filbcmb  26432  sdclem2  26452  sdclem1  26453  fdc1  26456  totbndbnd  26513  heibor1  26534  elrfirn2  26771  ofmpteq  26797  mzpsubst  26826  eq0rabdioph  26856  sbccomieg  26870  rexrabdioph  26875  rexfrabdioph  26876  rabdiophlem2  26883  elnn0rabdioph  26884  dvdsrabdioph  26891  rabrenfdioph  26897  fphpd  26899  monotuz  27026  monotoddzz  27028  oddcomabszz  27029  setindtrs  27118  wdom2d2  27128  fnwe2val  27146  fnwe2lem1  27147  aomclem6  27156  aomclem8  27159  flcidc  27379  mamufval  27443  compab  27644  evth2f  27686  elunif  27687  fvelrnbf  27689  rfcnpre1  27690  fsumcnf  27692  sumsnd  27697  evthf  27698  refsumcn  27701  rfcnpre2  27702  rfcnpre3  27704  rfcnpre4  27705  rfcnnnub  27707  refsum2cnlem1  27708  refsum2cn  27709  fmul01  27710  fmuldfeqlem1  27712  fmuldfeq  27713  fmul01lt1lem1  27714  fmul01lt1lem2  27715  fmul01lt1  27716  cncfmptss  27717  mulc1cncfg  27721  infrglb  27722  expcnfg  27726  climmulf  27730  climexp  27731  climsuse  27734  climrecf  27735  climinff  27737  dvcosre  27741  itgsin0pilem1  27744  ibliccsinexp  27745  itgsinexplem1  27748  itgsinexp  27749  stoweidlem3  27752  stoweidlem8  27757  stoweidlem14  27763  stoweidlem16  27765  stoweidlem18  27767  stoweidlem19  27768  stoweidlem21  27770  stoweidlem22  27771  stoweidlem23  27772  stoweidlem26  27775  stoweidlem27  27776  stoweidlem28  27777  stoweidlem29  27778  stoweidlem30  27779  stoweidlem31  27780  stoweidlem32  27781  stoweidlem34  27783  stoweidlem35  27784  stoweidlem36  27785  stoweidlem41  27790  stoweidlem42  27791  stoweidlem43  27792  stoweidlem44  27793  stoweidlem45  27794  stoweidlem46  27795  stoweidlem47  27796  stoweidlem48  27797  stoweidlem49  27798  stoweidlem51  27800  stoweidlem52  27801  stoweidlem53  27802  stoweidlem54  27803  stoweidlem55  27804  stoweidlem56  27805  stoweidlem57  27806  stoweidlem58  27807  stoweidlem59  27808  stoweidlem60  27809  stoweidlem62  27811  stowei  27813  wallispilem5  27818  wallispi  27819  stirlinglem2  27824  stirlinglem3  27825  stirlinglem4  27826  stirlinglem5  27827  stirlinglem8  27830  stirlinglem11  27833  stirlinglem12  27834  stirlinglem13  27835  stirlinglem14  27836  stirlinglem15  27837  stirling  27838  cbvral2  27950  cbvrex2  27951  raaan2  27953  2reurex  27959  2reu3  27966  2reu7  27969  2reu8  27970  nfafv  27999  mpt2xopoveq  28085  mpt2xopovel  28086  bnj23  28744  bnj1366  28862  bnj1379  28863  bnj1400  28868  bnj1534  28885  bnj1542  28889  bnj607  28948  bnj873  28956  bnj958  28972  bnj1000  28973  bnj981  28982  bnj1014  28992  bnj1123  29016  bnj1204  29042  bnj1388  29063  bnj1398  29064  bnj1408  29066  bnj1445  29074  bnj1446  29075  bnj1447  29076  bnj1448  29077  bnj1449  29078  bnj1466  29083  bnj1467  29084  bnj1463  29085  bnj1312  29088  bnj1498  29091  bnj1519  29095  bnj1520  29096  bnj1525  29099  bnj1529  29100  riotaocN  29399  cdleme26ee  30549  cdleme31sn1  30570  cdleme31se2  30572  cdlemefrs29bpre0  30585  cdlemefs32sn1aw  30603  cdleme43fsv1snlem  30609  cdleme41sn3a  30622  cdleme32d  30633  cdleme32f  30635  cdleme40m  30656  cdleme40n  30657  cdleme42b  30667  ltrniotaval  30770  cdlemksv2  31036  cdlemkuv2  31056  cdlemk36  31102  cdlemk38  31104  cdlemkid  31125  cdlemk19x  31132  cdlemk11t  31135  dihglblem5  31488  hlhilset  32127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-17 1603
This theorem depends on definitions:  df-bi 177  df-nf 1532  df-nfc 2408
  Copyright terms: Public domain W3C validator