Theorem nfsbc1v 3731

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

Syntax hints:  Ⅎwnf 1787  [wsbc 3711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-sbc 3712

This theorem is referenced by:  elrabsf  3759  cbvralcsf  3873  reusngf  4605  rexreusng  4612  reuprg0  4635  rmosn  4652  rabsnifsb  4655  euotd  5421  reuop  6185  frpoinsg  6231  wfisgOLD  6242  elfvmptrab1w  6883  elfvmptrab1  6884  ralrnmptw  6952  ralrnmpt  6954  oprabv  7313  elovmporab  7493  elovmporab1w  7494  elovmporab1  7495  ovmpt3rabdm  7506  elovmpt3rab1  7507  tfindes  7684  findes  7723  dfopab2  7865  dfoprab3s  7866  mpoxopoveq  8006  findcard2  8909  findcard2OLD  8986  ac6sfi  8988  indexfi  9057  frinsg  9440  nn0ind-raph  12350  uzind4s  12577  fzrevral  13270  rabssnn0fi  13634  prmind2  16318  elmptrab  22886  isfildlem  22916  2sqreulem4  26507  gropd  27304  grstructd  27305  rspc2daf  30717  opreu2reuALT  30726  bnj919  32647  bnj1468  32726  bnj110  32738  bnj607  32796  bnj873  32804  bnj849  32805  bnj1388  32913  bnj1489  32936  ralxpes  33581  ralxp3es  33591  setinds  33660  dfon2lem1  33665  tfisg  33692  frpoins3xpg  33714  frpoins3xp3g  33715  rdgssun  35476  indexa  35818  indexdom  35819  sdclem2  35827  sdclem1  35828  fdc1  35831  alrimii  36204  riotasv2s  36899  sbccomieg  40531  rexrabdioph  40532  rexfrabdioph  40533  aomclem6  40800  pm14.24  41939  or2expropbilem2  44414  or2expropbi  44415  ich2exprop  44811  ichnreuop  44812  ichreuopeq  44813  prproropreud  44849  reupr  44862  reuopreuprim  44866