Theorem nfsbc1v 3762

Description: Bound-variable hypothesis builder for class substitution. (Contributed by Mario Carneiro, 12-Oct-2016.)

Assertion

Ref	Expression
nfsbc1v	⊢ Ⅎ𝑥[𝐴 / 𝑥]𝜑

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem nfsbc1v

Step	Hyp	Ref	Expression
1		nfcv 2899	. 2 ⊢ Ⅎ𝑥𝐴
2	1	nfsbc1 3761	1 ⊢ Ⅎ𝑥[𝐴 / 𝑥]𝜑

Syntax hints:  Ⅎwnf 1785  [wsbc 3742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-sbc 3743

This theorem is referenced by:  elrabsf  3788  cbvralcsf  3893  reusngf  4633  rexreusng  4638  reuprg0  4661  rmosn  4678  rabsnifsb  4681  euotd  5471  reuop  6261  frpoinsg  6311  elfvmptrab1w  6979  elfvmptrab1  6980  ralrnmptw  7050  ralrnmpt  7052  oprabv  7430  elovmporab  7616  elovmporab1w  7617  elovmporab1  7618  ovmpt3rabdm  7629  elovmpt3rab1  7630  tfisg  7808  tfindes  7817  findes  7854  dfopab2  8008  dfoprab3s  8009  ralxpes  8090  ralxp3es  8093  frpoins3xpg  8094  frpoins3xp3g  8095  mpoxopoveq  8173  findcard2  9103  ac6sfi  9198  indexfi  9274  setinds  9672  frinsg  9677  nn0ind-raph  12606  uzind4s  12835  fzrevral  13542  rabssnn0fi  13923  prmind2  16626  elmptrab  23788  isfildlem  23818  2sqreulem4  27438  gropd  29122  grstructd  29123  rspc2daf  32558  opreu2reuALT  32569  bnj919  34950  bnj1468  35028  bnj110  35040  bnj607  35098  bnj873  35106  bnj849  35107  bnj1388  35215  bnj1489  35238  dfon2lem1  36003  rdgssun  37660  indexa  38013  indexdom  38014  sdclem2  38022  sdclem1  38023  fdc1  38026  alrimii  38399  riotasv2s  39363  sbccomieg  43179  rexrabdioph  43180  rexfrabdioph  43181  aomclem6  43445  pm14.24  44817  or2expropbilem2  47422  or2expropbi  47423  ich2exprop  47860  ichnreuop  47861  ichreuopeq  47862  prproropreud  47898  reupr  47911  reuopreuprim  47915