MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfcsb1v Structured version   Visualization version   GIF version

Theorem nfcsb1v 3582
Description: Bound-variable hypothesis builder for substitution into a class. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 12-Oct-2016.)
Assertion
Ref Expression
nfcsb1v 𝑥𝐴 / 𝑥𝐵
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem nfcsb1v
StepHypRef Expression
1 nfcv 2793 . 2 𝑥𝐴
21nfcsb1 3581 1 𝑥𝐴 / 𝑥𝐵
Colors of variables: wff setvar class
Syntax hints:  wnfc 2780  csb 3566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-sbc 3469  df-csb 3567
This theorem is referenced by:  csbhypf  3585  csbiebt  3586  cbvralcsf  3598  cbvreucsf  3600  cbvrabcsf  3601  sbcnestgf  4028  csbnest1g  4034  csbun  4042  csbin  4043  csbif  4171  disjors  4667  invdisjrab  4671  disjxiun  4681  disjxiunOLD  4682  disjxun  4683  sbcbr123  4739  eusvnf  4891  reusv2lem4  4902  reusv2  4904  moop2  4995  iunopeqop  5010  pofun  5080  opeliunxp  5204  elrnmpt1  5406  resmptf  5486  csbima12  5518  fvmpt2f  6322  fvmpts  6324  fvmpt2i  6329  fvmptex  6333  fmptco  6436  fmptcof  6437  fmptcos  6438  elabrex  6541  fliftfuns  6604  csbov123  6727  ovmpt2s  6826  ofmpteq  6958  mpt2mptsx  7278  dmmpt2ssx  7280  fmpt2x  7281  el2mpt2csbcl  7295  offval22  7298  ovmptss  7303  fmpt2co  7305  dfmpt2  7312  mpt2xeldm  7382  mpt2curryd  7440  mpt2curryvald  7441  fvmpt2curryd  7442  eqerlem  7821  qliftfuns  7877  mptelixpg  7987  boxcutc  7993  xpf1o  8163  iunfi  8295  wdom2d  8526  ixpiunwdom  8537  hsmexlem2  9287  ac6num  9339  ac6c4  9341  iundom2g  9400  seqof2  12899  rlimcld2  14353  nfsum1  14464  sumeq2ii  14467  summolem3  14489  summolem2a  14490  zsum  14493  fsum  14495  sumss2  14501  fsumcvg2  14502  fsumzcl2  14513  fsumsplitf  14516  sumsnf  14517  sumsn  14519  sumsns  14523  fsummsnunz  14527  fsumsplitsnun  14528  fsummsnunzOLD  14529  fsumsplitsnunOLD  14530  fsum2dlem  14545  fsumcom2  14549  fsumcom2OLD  14550  fsumshftm  14557  fsum0diag2  14559  fsum00  14574  fsumabs  14577  fsumrlim  14587  fsumo1  14588  o1fsum  14589  fsumiun  14597  infcvgaux1i  14633  nfcprod1  14684  prodeq2ii  14687  prodmolem3  14707  prodmolem2a  14708  zprod  14711  fprod  14715  fprodntriv  14716  prodss  14721  fprodser  14723  fprodcllemf  14732  prodsn  14736  prodsnf  14738  fprodm1s  14744  fprodp1s  14745  prodsns  14746  fprodabs  14748  fprodn0  14753  fprod2dlem  14754  fprodcom2  14758  fprodcom2OLD  14759  fproddivf  14762  fprodsplitf  14763  fprodle  14771  fprodmodd  14772  fprodefsum  14869  sumeven  15157  sumodd  15158  pcmpt  15643  pcmptdvds  15645  natpropd  16683  fucpropd  16684  gsummpt1n0  18410  gsumcom2  18420  gsummptnn0fz  18428  dprd2d2  18489  psrass1lem  19425  mpfrcl  19566  coe1fzgsumdlem  19719  gsummoncoe1  19722  gsumply1eq  19723  evl1gsumdlem  19768  mdetralt2  20463  mdetunilem2  20467  madugsum  20497  fiuncmp  21255  ptcld  21464  ptcldmpt  21465  ptclsg  21466  elmptrab  21678  prdsdsf  22219  prdsxmet  22221  fsumcn  22720  fsum2cn  22721  ovolfiniun  23315  ovoliunlem3  23318  ovoliun  23319  ovoliun2  23320  ovoliunnul  23321  finiunmbl  23358  volfiniun  23361  iundisj  23362  iundisj2  23363  iunmbl  23367  iunmbl2  23371  itgss3  23626  itgfsum  23638  itgabs  23646  limciun  23703  dvmptfsum  23783  dvfsumle  23829  dvfsumabs  23831  dvfsumlem1  23834  dvfsumlem2  23835  dvfsumlem3  23836  dvfsumlem4  23837  dvfsumrlim  23839  dvfsumrlim2  23840  dvfsum2  23842  itgsubstlem  23856  itgsubst  23857  rlimcnp2  24738  fsumdvdscom  24956  fsumdvdsmul  24966  fsumvma  24983  dchrisumlema  25222  dchrisumlem2  25224  dchrisumlem3  25225  rspc2vd  27245  disjorsf  29519  disjabrex  29521  disjabrexf  29522  iundisjf  29528  iundisj2f  29529  disjunsn  29533  suppss2f  29567  fmptdF  29584  fmptcof2  29585  acunirnmpt2f  29589  aciunf1lem  29590  funcnv4mpt  29598  f1od2  29627  iundisjfi  29683  iundisj2fi  29684  fsumiunle  29703  gsummpt2co  29908  gsumvsca1  29910  gsumvsca2  29911  esumpfinvalf  30266  esum2dlem  30282  esumiun  30284  fiunelros  30365  measiun  30409  voliune  30420  volfiniune  30421  sbcaltop  32213  bj-sbeqALT  33020  csbdif  33301  phpreu  33523  finixpnum  33524  ptrest  33538  poimirlem23  33562  poimirlem24  33563  poimirlem25  33564  poimirlem26  33565  poimirlem27  33566  poimirlem28  33567  mbfposadd  33587  itgabsnc  33609  ftc1cnnclem  33613  ftc2nc  33624  fsumshftd  34556  riotasv2s  34562  cdleme31sn  35985  cdleme31sn1  35986  cdleme31se2  35988  cdleme32fva  36042  cdleme42b  36083  hlhilset  37543  mzpsubst  37628  rabdiophlem2  37683  elnn0rabdioph  37684  dvdsrabdioph  37691  fphpd  37697  monotuz  37823  oddcomabszz  37826  wdom2d2  37919  aomclem6  37946  flcidc  38061  csbcog  38258  csbingOLD  39369  fsumcnf  39494  sumsnd  39499  elabrexg  39520  fiiuncl  39548  eliin2f  39601  disjf1  39683  disjrnmpt2  39689  disjinfi  39694  fmptf  39762  iuneqfzuzlem  39863  supxrleubrnmptf  39993  fsumclf  40119  fsummulc1f  40120  fsumnncl  40121  fsumf1of  40124  fsumiunss  40125  fsumreclf  40126  fsumlessf  40127  fprodexp  40144  fprodabs2  40145  mccllem  40147  fprodcnlem  40149  fprodcn  40150  climeldmeqmpt  40218  climeldmeqmpt3  40239  climinf2mpt  40264  climinfmpt  40265  limsupequzmptf  40281  fprodcncf  40432  dvmptmulf  40470  dvnmptdivc  40471  dvmptfprod  40478  iblsplitf  40504  fourierdlem86  40727  fourierdlem112  40753  sge0iunmptlemfi  40948  sge0iunmptlemre  40950  sge0iunmpt  40953  sge0ltfirpmpt2  40961  sge0isummpt2  40967  sge0xaddlem2  40969  sge0xadd  40970  hoimbl2  41200  vonn0ioo2  41225  vonn0icc2  41227  csbafv12g  41538  csbaovg  41581  fsummsndifre  41667  fsumsplitsndif  41668  fsummmodsndifre  41669  fsummmodsnunz  41670  opeliun2xp  42436  dmmpt2ssx2  42440
  Copyright terms: Public domain W3C validator