Theorem nfsbc1v 3773

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

Syntax hints:  Ⅎwnf 1810  [wsbc 3753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-sbc 3754

This theorem is referenced by:  elrabsf  3798  cbvralcsf  3903  reusngf  4645  rexreusng  4650  reuprg0  4673  rmosn  4690  rabsnifsb  4693  euotd  5497  reuop  6295  frpoinsg  6345  elfvmptrab1w  7018  elfvmptrab1  7019  ralrnmptw  7090  ralrnmpt  7092  oprabv  7471  elovmporab  7657  elovmporab1w  7658  elovmporab1  7659  ovmpt3rabdm  7670  elovmpt3rab1  7671  tfisg  7850  tfindes  7859  findes  7897  dfopab2  8049  dfoprab3s  8050  ralxpes  8132  ralxp3es  8135  frpoins3xpg  8136  frpoins3xp3g  8137  mpoxopoveq  8215  findcard2  9149  ac6sfi  9244  indexfi  9317  setinds  9718  frinsg  9723  nn0ind-raph  12696  uzind4s  12932  fzrevral  13640  rabssnn0fi  14022  prmind2  16743  elmptrab  23953  isfildlem  23983  2sqreulem4  27584  gropd  29322  grstructd  29323  rspc2daf  32754  opreu2reuALT  32764  bnj919  35101  bnj1468  35179  bnj110  35191  bnj607  35249  bnj873  35257  bnj849  35258  bnj1388  35366  bnj1489  35389  dfon2lem1  36206  rdgssun  37946  indexa  38306  indexdom  38307  sdclem2  38315  sdclem1  38316  fdc1  38319  alrimii  38692  riotasv2s  39656  sbccomieg  43446  rexrabdioph  43447  rexfrabdioph  43448  aomclem6  43712  pm14.24  45068  or2expropbilem2  47693  or2expropbi  47694  ich2exprop  48143  ichnreuop  48144  ichreuopeq  48145  prproropreud  48181  reupr  48194  reuopreuprim  48198