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

Theorem nfcsb1v 3910
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 2981 . 2 𝑥𝐴
21nfcsb1 3909 1 𝑥𝐴 / 𝑥𝐵
Colors of variables: wff setvar class
Syntax hints:  wnfc 2965  csb 3886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-sbc 3776  df-csb 3887
This theorem is referenced by:  csbhypf  3914  csbiebt  3915  cbvrabcsfw  3927  cbvralcsf  3928  cbvreucsf  3930  cbvrabcsf  3931  rspc2vd  3935  sbcnestgfw  4373  sbcnestgf  4378  csbnest1g  4384  csbun  4393  csbin  4394  csbif  4524  disjors  5043  invdisjrabw  5047  invdisjrab  5048  disjxiun  5059  disjxun  5060  sbcbr123  5116  eusvnf  5288  reusv2lem4  5297  reusv2  5299  moop2  5388  iunopeqop  5407  pofun  5489  opeliunxp  5617  elrnmpt1  5828  resmptf  5905  csbima12  5944  fvmpt2f  6765  fvmpts  6767  fvmpt2i  6773  fvmptex  6777  fmptco  6886  fmptcof  6887  fmptcos  6888  elabrex  6999  fliftfuns  7062  csbov123  7193  ovmpos  7291  ofmpteq  7421  mpomptsx  7756  dmmpossx  7758  fmpox  7759  el2mpocsbcl  7774  offval22  7777  ovmptss  7782  fmpoco  7784  dfmpo  7791  mpoxeldm  7871  mpocurryd  7929  mpocurryvald  7930  fvmpocurryd  7931  eqerlem  8316  qliftfuns  8377  mptelixpg  8491  boxcutc  8497  xpf1o  8671  iunfi  8804  wdom2d  9036  ixpiunwdom  9047  hsmexlem2  9841  ac6c4  9895  iundom2g  9954  seqof2  13421  rlimcld2  14928  nfsum1  15039  sumeq2ii  15043  summolem3  15064  summolem2a  15065  zsum  15068  fsum  15070  sumss2  15076  fsumcvg2  15077  fsumzcl2  15088  fsumsplitf  15091  sumsnf  15092  sumsns  15098  fsummsnunz  15102  fsumsplitsnun  15103  fsum2dlem  15118  fsumcom2  15122  fsumshftm  15129  fsum0diag2  15131  fsum00  15146  fsumabs  15149  fsumrlim  15159  fsumo1  15160  o1fsum  15161  fsumiun  15169  infcvgaux1i  15205  nfcprod1  15257  prodeq2ii  15260  prodmolem3  15280  prodmolem2a  15281  zprod  15284  fprod  15288  fprodntriv  15289  prodss  15294  fprodser  15296  fprodcllemf  15305  prodsn  15309  prodsnf  15311  fprodm1s  15317  fprodp1s  15318  prodsns  15319  fprodabs  15321  fprodn0  15326  fprod2dlem  15327  fprodcom2  15331  fproddivf  15334  fprodsplitf  15335  fprodsplit1f  15337  fprodle  15343  fprodmodd  15344  fprodefsum  15441  sumeven  15731  sumodd  15732  pcmpt  16221  pcmptdvds  16223  natpropd  17239  fucpropd  17240  gsummpt1n0  19008  gsumcom2  19018  gsummptnn0fz  19029  dprd2d2  19089  psrass1lem  20079  mpfrcl  20219  coe1fzgsumdlem  20389  gsummoncoe1  20392  gsumply1eq  20393  evl1gsumdlem  20438  mdetralt2  21137  mdetunilem2  21141  madugsum  21171  fiuncmp  21931  ptcld  22140  ptcldmpt  22141  ptclsg  22142  elmptrab  22354  prdsdsf  22895  prdsxmet  22897  fsumcn  23396  fsum2cn  23397  ovolfiniun  24020  ovoliunlem3  24023  ovoliun  24024  ovoliun2  24025  ovoliunnul  24026  finiunmbl  24063  volfiniun  24066  iundisj  24067  iundisj2  24068  iunmbl  24072  iunmbl2  24076  itgss3  24333  itgfsum  24345  itgabs  24353  limciun  24410  dvmptfsum  24490  dvfsumle  24536  dvfsumabs  24538  dvfsumlem1  24541  dvfsumlem2  24542  dvfsumlem3  24543  dvfsumlem4  24544  dvfsumrlim  24546  dvfsumrlim2  24547  dvfsum2  24549  itgsubstlem  24563  itgsubst  24564  rlimcnp2  25461  fsumdvdscom  25679  fsumdvdsmul  25689  fsumvma  25706  dchrisumlema  25981  dchrisumlem2  25983  dchrisumlem3  25984  disjorsf  30248  disjabrex  30250  disjabrexf  30251  iundisjf  30257  iundisj2f  30258  disjunsn  30262  suppss2f  30302  fmptdF  30319  fmptcof2  30320  acunirnmpt2f  30324  aciunf1lem  30325  funcnv4mpt  30332  f1od2  30373  iundisjfi  30435  iundisj2fi  30436  fsumiunle  30462  gsummpt2co  30603  gsumvsca1  30771  gsumvsca2  30772  rmfsupp2  30783  esumpfinvalf  31224  esum2dlem  31240  esumiun  31242  fiunelros  31322  measiun  31366  voliune  31377  volfiniune  31378  sbcaltop  33329  bj-sbeqALT  34104  csbdif  34478  phpreu  34746  finixpnum  34747  ptrest  34761  poimirlem23  34785  poimirlem24  34786  poimirlem25  34787  poimirlem26  34788  poimirlem27  34789  poimirlem28  34790  mbfposadd  34809  itgabsnc  34831  ftc1cnnclem  34835  ftc2nc  34846  fsumshftd  35958  riotasv2s  35964  cdleme31sn  37386  cdleme31sn1  37387  cdleme31se2  37389  cdleme32fva  37443  cdleme42b  37484  hlhilset  38940  mzpsubst  39213  rabdiophlem2  39267  elnn0rabdioph  39268  dvdsrabdioph  39275  fphpd  39281  monotuz  39406  oddcomabszz  39409  wdom2d2  39500  aomclem6  39527  flcidc  39642  csbcog  39862  fsumcnf  41146  sumsnd  41151  elabrexg  41171  fiiuncl  41195  eliin2f  41239  disjf1  41311  disjrnmpt2  41317  disjinfi  41322  fmptf  41377  iuneqfzuzlem  41470  supxrleubrnmptf  41595  fsumclf  41718  fsummulc1f  41719  fsumnncl  41720  fsumf1of  41723  fsumiunss  41724  fsumreclf  41725  fsumlessf  41726  fprodexp  41743  fprodabs2  41744  mccllem  41746  fprodcnlem  41748  fprodcn  41749  climeldmeqmpt  41817  climeldmeqmpt3  41838  climinf2mpt  41863  climinfmpt  41864  limsupequzmptf  41880  fprodcncf  42052  dvmptmulf  42090  dvnmptdivc  42091  dvmptfprod  42098  iblsplitf  42123  fourierdlem86  42346  fourierdlem112  42372  sge0iunmptlemfi  42564  sge0iunmptlemre  42566  sge0iunmpt  42569  sge0ltfirpmpt2  42577  sge0isummpt2  42583  sge0xaddlem2  42585  sge0xadd  42586  hoimbl2  42816  vonn0ioo2  42841  vonn0icc2  42843  csbafv12g  43205  csbaovg  43248  csbafv212g  43287  fsummsndifre  43401  fsumsplitsndif  43402  fsummmodsndifre  43403  fsummmodsnunz  43404  opeliun2xp  44216  dmmpossx2  44220
  Copyright terms: Public domain W3C validator