Theorem nfsbc1v 3760

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 2898	. 2 ⊢ Ⅎ𝑥𝐴
2	1	nfsbc1 3759	1 ⊢ Ⅎ𝑥[𝐴 / 𝑥]𝜑

Syntax hints:  Ⅎwnf 1784  [wsbc 3740

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-sbc 3741

This theorem is referenced by:  elrabsf  3786  cbvralcsf  3891  reusngf  4631  rexreusng  4636  reuprg0  4659  rmosn  4676  rabsnifsb  4679  euotd  5461  reuop  6251  frpoinsg  6301  elfvmptrab1w  6968  elfvmptrab1  6969  ralrnmptw  7039  ralrnmpt  7041  oprabv  7418  elovmporab  7604  elovmporab1w  7605  elovmporab1  7606  ovmpt3rabdm  7617  elovmpt3rab1  7618  tfisg  7796  tfindes  7805  findes  7842  dfopab2  7996  dfoprab3s  7997  ralxpes  8078  ralxp3es  8081  frpoins3xpg  8082  frpoins3xp3g  8083  mpoxopoveq  8161  findcard2  9091  ac6sfi  9186  indexfi  9262  setinds  9660  frinsg  9665  nn0ind-raph  12594  uzind4s  12823  fzrevral  13530  rabssnn0fi  13911  prmind2  16614  elmptrab  23773  isfildlem  23803  2sqreulem4  27423  gropd  29106  grstructd  29107  rspc2daf  32542  opreu2reuALT  32553  bnj919  34925  bnj1468  35004  bnj110  35016  bnj607  35074  bnj873  35082  bnj849  35083  bnj1388  35191  bnj1489  35214  dfon2lem1  35977  rdgssun  37585  indexa  37936  indexdom  37937  sdclem2  37945  sdclem1  37946  fdc1  37949  alrimii  38322  riotasv2s  39240  sbccomieg  43056  rexrabdioph  43057  rexfrabdioph  43058  aomclem6  43322  pm14.24  44694  or2expropbilem2  47300  or2expropbi  47301  ich2exprop  47738  ichnreuop  47739  ichreuopeq  47740  prproropreud  47776  reupr  47789  reuopreuprim  47793