Theorem nfsbc1v 3748

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

Syntax hints:  Ⅎwnf 1785  [wsbc 3728

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-sbc 3729

This theorem is referenced by:  elrabsf  3774  cbvralcsf  3879  reusngf  4618  rexreusng  4623  reuprg0  4646  rmosn  4663  rabsnifsb  4666  euotd  5467  reuop  6257  frpoinsg  6307  elfvmptrab1w  6975  elfvmptrab1  6976  ralrnmptw  7046  ralrnmpt  7048  oprabv  7427  elovmporab  7613  elovmporab1w  7614  elovmporab1  7615  ovmpt3rabdm  7626  elovmpt3rab1  7627  tfisg  7805  tfindes  7814  findes  7851  dfopab2  8005  dfoprab3s  8006  ralxpes  8086  ralxp3es  8089  frpoins3xpg  8090  frpoins3xp3g  8091  mpoxopoveq  8169  findcard2  9099  ac6sfi  9194  indexfi  9270  setinds  9670  frinsg  9675  nn0ind-raph  12629  uzind4s  12858  fzrevral  13566  rabssnn0fi  13948  prmind2  16654  elmptrab  23792  isfildlem  23822  2sqreulem4  27417  gropd  29100  grstructd  29101  rspc2daf  32535  opreu2reuALT  32546  bnj919  34910  bnj1468  34988  bnj110  35000  bnj607  35058  bnj873  35066  bnj849  35067  bnj1388  35175  bnj1489  35198  dfon2lem1  35963  rdgssun  37694  indexa  38054  indexdom  38055  sdclem2  38063  sdclem1  38064  fdc1  38067  alrimii  38440  riotasv2s  39404  sbccomieg  43221  rexrabdioph  43222  rexfrabdioph  43223  aomclem6  43487  pm14.24  44859  or2expropbilem2  47481  or2expropbi  47482  ich2exprop  47931  ichnreuop  47932  ichreuopeq  47933  prproropreud  47969  reupr  47982  reuopreuprim  47986