Theorem nfsbc1v 3811

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 3810	1 ⊢ Ⅎ𝑥[𝐴 / 𝑥]𝜑

Syntax hints:  Ⅎwnf 1780  [wsbc 3791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-sbc 3792

This theorem is referenced by:  elrabsf  3840  cbvralcsf  3953  reusngf  4679  rexreusng  4684  reuprg0  4707  rmosn  4724  rabsnifsb  4727  euotd  5523  reuop  6315  frpoinsg  6366  wfisgOLD  6377  elfvmptrab1w  7043  elfvmptrab1  7044  ralrnmptw  7114  ralrnmpt  7116  oprabv  7493  elovmporab  7679  elovmporab1w  7680  elovmporab1  7681  ovmpt3rabdm  7692  elovmpt3rab1  7693  tfisg  7875  tfindes  7884  findes  7923  dfopab2  8076  dfoprab3s  8077  ralxpes  8160  ralxp3es  8163  frpoins3xpg  8164  frpoins3xp3g  8165  mpoxopoveq  8243  findcard2  9203  ac6sfi  9318  indexfi  9398  frinsg  9789  nn0ind-raph  12716  uzind4s  12948  fzrevral  13649  rabssnn0fi  14024  prmind2  16719  elmptrab  23851  isfildlem  23881  2sqreulem4  27513  gropd  29063  grstructd  29064  rspc2daf  32495  opreu2reuALT  32505  bnj919  34760  bnj1468  34839  bnj110  34851  bnj607  34909  bnj873  34917  bnj849  34918  bnj1388  35026  bnj1489  35049  setinds  35760  dfon2lem1  35765  rdgssun  37361  indexa  37720  indexdom  37721  sdclem2  37729  sdclem1  37730  fdc1  37733  alrimii  38106  riotasv2s  38940  sbccomieg  42781  rexrabdioph  42782  rexfrabdioph  42783  aomclem6  43048  pm14.24  44428  or2expropbilem2  46983  or2expropbi  46984  ich2exprop  47396  ichnreuop  47397  ichreuopeq  47398  prproropreud  47434  reupr  47447  reuopreuprim  47451