Theorem nfsbc1v 3797

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

Syntax hints:  Ⅎwnf 1785  [wsbc 3777

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-sbc 3778

This theorem is referenced by:  elrabsf  3825  cbvralcsf  3938  reusngf  4676  rexreusng  4683  reuprg0  4706  rmosn  4723  rabsnifsb  4726  euotd  5513  reuop  6292  frpoinsg  6344  wfisgOLD  6355  elfvmptrab1w  7024  elfvmptrab1  7025  ralrnmptw  7095  ralrnmpt  7097  oprabv  7471  elovmporab  7654  elovmporab1w  7655  elovmporab1  7656  ovmpt3rabdm  7667  elovmpt3rab1  7668  tfisg  7845  tfindes  7854  findes  7895  dfopab2  8040  dfoprab3s  8041  ralxpes  8124  ralxp3es  8127  frpoins3xpg  8128  frpoins3xp3g  8129  mpoxopoveq  8206  findcard2  9166  findcard2OLD  9286  ac6sfi  9289  indexfi  9362  frinsg  9748  nn0ind-raph  12666  uzind4s  12896  fzrevral  13590  rabssnn0fi  13955  prmind2  16626  elmptrab  23551  isfildlem  23581  2sqreulem4  27181  gropd  28546  grstructd  28547  rspc2daf  31963  opreu2reuALT  31972  bnj919  34064  bnj1468  34143  bnj110  34155  bnj607  34213  bnj873  34221  bnj849  34222  bnj1388  34330  bnj1489  34353  setinds  35042  dfon2lem1  35047  rdgssun  36562  indexa  36904  indexdom  36905  sdclem2  36913  sdclem1  36914  fdc1  36917  alrimii  37290  riotasv2s  38131  sbccomieg  41833  rexrabdioph  41834  rexfrabdioph  41835  aomclem6  42103  pm14.24  43493  or2expropbilem2  46042  or2expropbi  46043  ich2exprop  46438  ichnreuop  46439  ichreuopeq  46440  prproropreud  46476  reupr  46489  reuopreuprim  46493