Theorem nfcsb1v 3091

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

Step	Hyp	Ref	Expression
1		nfcv 2319	. 2 |- F/_ x A
2	1	nfcsb1 3090	1 |- F/_ x [_ A / x ]_ B

Syntax hints:   F/_wnfc 2306   [_csb 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-sbc 2964  df-csb 3059

This theorem is referenced by:  csbhypf  3096  csbiebt  3097  sbcnestgf  3109  csbnest1g  3113  cbvralcsf  3120  cbvrexcsf  3121  cbvreucsf  3122  cbvrabcsf  3123  rspc2vd  3126  csbing  3343  disjnims  3996  disjiun  3999  sbcbrg  4058  moop2  4252  pofun  4313  eusvnf  4454  opeliunxp  4682  elrnmpt1  4879  resmptf  4958  csbima12g  4990  fvmpts  5595  fvmpt2  5600  mptfvex  5602  fmptco  5683  fmptcof  5684  fmptcos  5685  elabrex  5759  fliftfuns  5799  csbov123g  5913  ovmpos  5998  mpomptsx  6198  dmmpossx  6200  fmpox  6201  mpofvex  6204  fmpoco  6217  dfmpo  6224  f1od2  6236  disjxp1  6237  eqerlem  6566  qliftfuns  6619  mptelixpg  6734  xpf1o  6844  iunfidisj  6945  cc3  7267  seq3f1olemstep  10501  seq3f1olemp  10502  nfsum1  11364  sumeq2  11367  sumfct  11382  sumrbdclem  11385  summodclem3  11388  summodclem2a  11389  zsumdc  11392  fsumgcl  11394  fsum3  11395  isumss  11399  isumss2  11401  fsum3cvg2  11402  fsumzcl2  11413  fsumsplitf  11416  sumsnf  11417  sumsns  11423  fsumsplitsnun  11427  fsum2dlemstep  11442  fisumcom2  11446  fsumshftm  11453  fisum0diag2  11455  fsummulc2  11456  fsum00  11470  fsumabs  11473  fsumrelem  11479  fsumiun  11485  isumshft  11498  mertenslem2  11544  nfcprod1  11562  prodeq2  11565  prodrbdclem  11579  prodmodclem3  11583  prodmodclem2a  11584  zproddc  11587  fprodseq  11591  fprodntrivap  11592  prodfct  11595  prodssdc  11597  fprodmul  11599  prodsnf  11600  fprodm1s  11609  fprodp1s  11610  prodsns  11611  fprodcl2lem  11613  fprodcllemf  11621  fprodabs  11624  fprodap0  11629  fprod2dlemstep  11630  fprodcom2fi  11634  fprodrec  11637  fproddivapf  11639  fprodsplitf  11640  fprodsplit1f  11642  fprodap0f  11644  fprodle  11648  fprodmodd  11649  pcmpt  12341  pcmptdvds  12343  ctiunctlemudc  12438  ctiunctlemf  12439  ctiunct  12441  ctiunctal  12442  iuncld  13618  fsumcncntop  14059  limcmpted  14135