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

Theorem nfcsb1v 3292
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  |-  F/_ x [_ A  /  x ]_ B
Distinct variable group:    x, A
Allowed substitution hint:    B( x)

Proof of Theorem nfcsb1v
StepHypRef Expression
1 nfcv 2569 . 2  |-  F/_ x A
21nfcsb1 3291 1  |-  F/_ x [_ A  /  x ]_ B
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2556   [_csb 3276
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-sbc 3176  df-csb 3277
This theorem is referenced by:  csbhypf  3295  csbiebt  3296  cbvralcsf  3307  cbvreucsf  3309  cbvrabcsf  3310  sbcnestgf  3679  csbnest1g  3685  csbun  3697  csbungOLD  3698  csbin  3700  csbingOLD  3701  csbif  3827  csbifgOLD  3828  csbopg  4065  disjors  4266  disjxiun  4277  disjxun  4278  sbcbr123  4331  sbcbrgOLD  4332  eusvnf  4475  reusv2lem4  4484  reusv2  4486  moop2  4574  pofun  4644  opeliunxp  4877  elrnmpt1  5075  csbima12  5174  csbima12gOLD  5175  fvmpts  5764  fvmpt2i  5768  fvmptex  5772  fmptco  5863  fmptcof  5864  fmptcos  5865  elabrex  5947  fliftfuns  5994  csbov123  6111  csbovgOLD  6113  ovmpt2s  6203  ofmpteq  6327  mpt2mptsx  6626  dmmpt2ssx  6628  fmpt2x  6629  offval22  6641  ovmptss  6643  fmpt2co  6645  dfmpt2  6652  eqerlem  7121  qliftfuns  7175  mptelixpg  7288  boxcutc  7294  xpf1o  7461  iunfi  7587  wdom2d  7783  ixpiunwdom  7794  hsmexlem2  8584  ac6num  8636  ac6c4  8638  iundom2g  8692  seqof2  11847  rlimcld2  13039  nfsum1  13150  sumeq2w  13152  sumeq2ii  13153  summolem3  13174  summolem2a  13175  zsum  13178  fsum  13180  sumss2  13186  fsumcvg2  13187  sumsn  13200  sumsns  13202  fsum2dlem  13220  fsumcom2  13224  fsumshftm  13230  fsum0diag2  13232  fsum00  13243  fsumabs  13246  fsumrlim  13256  fsumo1  13257  o1fsum  13258  fsumiun  13266  infcvgaux1i  13301  pcmpt  13936  pcmptdvds  13938  natpropd  14868  fucpropd  14869  gsumcom2  16440  dprd2d2  16516  psrass1lem  17380  mdetralt2  18256  mdetunilem2  18260  madugsum  18290  fiuncmp  18848  ptcld  19027  ptcldmpt  19028  ptclsg  19029  elmptrab  19241  prdsdsf  19783  prdsxmet  19785  fsumcn  20287  fsum2cn  20288  ovolfiniun  20825  ovoliunlem3  20828  ovoliun  20829  ovoliun2  20830  ovoliunnul  20831  finiunmbl  20866  volfiniun  20869  iundisj  20870  iundisj2  20871  iunmbl  20875  iunmbl2  20879  itgss3  21133  itgfsum  21145  itgabs  21153  limciun  21210  dvmptfsum  21288  dvfsumle  21334  dvfsumabs  21336  dvfsumlem1  21339  dvfsumlem2  21340  dvfsumlem3  21341  dvfsumlem4  21342  dvfsumrlim  21344  dvfsumrlim2  21345  dvfsum2  21347  itgsubstlem  21361  itgsubst  21362  mpfrcl  21369  rlimcnp2  22244  fsumdvdscom  22409  fsumdvdsmul  22419  fsumvma  22436  dchrisumlema  22621  dchrisumlem2  22623  dchrisumlem3  22624  disjorsf  25747  disjabrex  25749  disjabrexf  25750  iundisjf  25754  iundisj2f  25755  suppss2f  25777  fmptdF  25795  resmptf  25797  fvmpt2f  25798  fmptcof2  25802  funcnv4mpt  25812  iundisjfi  25902  iundisj2fi  25903  gsummpt2co  26100  gsumvsca1  26103  gsumvsca2  26104  esumpfinvalf  26378  measiun  26485  voliune  26498  volfiniune  26499  nfcprod1  27269  prodeq2w  27271  prodeq2ii  27272  prodmolem3  27292  prodmolem2a  27293  zprod  27296  fprod  27300  fprodntriv  27301  prodss  27306  fprodser  27308  prodsn  27319  fprodm1s  27326  fprodp1s  27327  prodsns  27328  fprodabs  27330  fprodefsum  27331  fprodn0  27336  fprod2dlem  27337  fprodcom2  27341  sbcaltop  27858  finixpnum  28255  ptrest  28266  mbfposadd  28280  itgabsnc  28302  ftc1cnnclem  28306  ftc2nc  28317  mzpsubst  28927  rabdiophlem2  28982  elnn0rabdioph  28983  dvdsrabdioph  28990  fphpd  28997  monotuz  29124  oddcomabszz  29127  wdom2d2  29226  aomclem6  29254  flcidc  29373  fsumcnf  29585  sumsnd  29590  csbafv12g  29886  csbaovg  29929  fsumz  30079  fsummsndifre  30080  fsumsplitsndif  30081  fsummmodsndifre  30082  fsummsnunz  30084  fsumsplitsnun  30085  fsummmodsnunre  30086  opeliun2xp  30562  dmmpt2ssx2  30568  bj-sbeqALT  31993  riotasv2s  32179  cdleme31sn  33594  cdleme31sn1  33595  cdleme31se2  33597  cdleme32fva  33651  cdleme42b  33692  hlhilset  35152
  Copyright terms: Public domain W3C validator