Theorem nfsbc1v 3818

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

Syntax hints:  Ⅎwnf 1781  [wsbc 3798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2105  ax-9 2113  ax-10 2136  ax-11 2153  ax-12 2173  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2890  df-sbc 3799

This theorem is referenced by:  elrabsf  3847  cbvralcsf  3960  reusngf  4696  rexreusng  4703  reuprg0  4727  rmosn  4744  rabsnifsb  4747  euotd  5536  reuop  6323  frpoinsg  6374  wfisgOLD  6385  elfvmptrab1w  7054  elfvmptrab1  7055  ralrnmptw  7126  ralrnmpt  7128  oprabv  7506  elovmporab  7692  elovmporab1w  7693  elovmporab1  7694  ovmpt3rabdm  7705  elovmpt3rab1  7706  tfisg  7887  tfindes  7896  findes  7936  dfopab2  8089  dfoprab3s  8090  ralxpes  8173  ralxp3es  8176  frpoins3xpg  8177  frpoins3xp3g  8178  mpoxopoveq  8256  findcard2  9226  ac6sfi  9344  indexfi  9426  frinsg  9816  nn0ind-raph  12739  uzind4s  12969  fzrevral  13665  rabssnn0fi  14033  prmind2  16726  elmptrab  23849  isfildlem  23879  2sqreulem4  27507  gropd  29057  grstructd  29058  rspc2daf  32486  opreu2reuALT  32496  bnj919  34735  bnj1468  34814  bnj110  34826  bnj607  34884  bnj873  34892  bnj849  34893  bnj1388  35001  bnj1489  35024  setinds  35734  dfon2lem1  35739  rdgssun  37292  indexa  37641  indexdom  37642  sdclem2  37650  sdclem1  37651  fdc1  37654  alrimii  38027  riotasv2s  38862  sbccomieg  42686  rexrabdioph  42687  rexfrabdioph  42688  aomclem6  42956  pm14.24  44341  or2expropbilem2  46882  or2expropbi  46883  ich2exprop  47277  ichnreuop  47278  ichreuopeq  47279  prproropreud  47315  reupr  47328  reuopreuprim  47332