Theorem nfsbc1v 3824

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

Syntax hints:  Ⅎwnf 1781  [wsbc 3804

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 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

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 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-sbc 3805

This theorem is referenced by:  elrabsf  3853  cbvralcsf  3966  reusngf  4696  rexreusng  4703  reuprg0  4727  rmosn  4744  rabsnifsb  4747  euotd  5532  reuop  6324  frpoinsg  6375  wfisgOLD  6386  elfvmptrab1w  7056  elfvmptrab1  7057  ralrnmptw  7128  ralrnmpt  7130  oprabv  7510  elovmporab  7696  elovmporab1w  7697  elovmporab1  7698  ovmpt3rabdm  7709  elovmpt3rab1  7710  tfisg  7891  tfindes  7900  findes  7940  dfopab2  8093  dfoprab3s  8094  ralxpes  8177  ralxp3es  8180  frpoins3xpg  8181  frpoins3xp3g  8182  mpoxopoveq  8260  findcard2  9230  ac6sfi  9348  indexfi  9430  frinsg  9820  nn0ind-raph  12743  uzind4s  12973  fzrevral  13669  rabssnn0fi  14037  prmind2  16732  elmptrab  23856  isfildlem  23886  2sqreulem4  27516  gropd  29066  grstructd  29067  rspc2daf  32495  opreu2reuALT  32505  bnj919  34743  bnj1468  34822  bnj110  34834  bnj607  34892  bnj873  34900  bnj849  34901  bnj1388  35009  bnj1489  35032  setinds  35742  dfon2lem1  35747  rdgssun  37344  indexa  37693  indexdom  37694  sdclem2  37702  sdclem1  37703  fdc1  37706  alrimii  38079  riotasv2s  38914  sbccomieg  42749  rexrabdioph  42750  rexfrabdioph  42751  aomclem6  43016  pm14.24  44401  or2expropbilem2  46948  or2expropbi  46949  ich2exprop  47345  ichnreuop  47346  ichreuopeq  47347  prproropreud  47383  reupr  47396  reuopreuprim  47400