Theorem nfsbc1v 3740

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

Syntax hints:  Ⅎwnf 1785  [wsbc 3720

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-sbc 3721

This theorem is referenced by:  elrabsf  3764  cbvralcsf  3870  vtocl2dOLD  3876  reusngf  4572  rexreusng  4577  reuprg0  4598  rmosn  4615  rabsnifsb  4618  euotd  5368  reuop  6112  wfisg  6151  elfvmptrab1w  6771  elfvmptrab1  6772  ralrnmptw  6837  ralrnmpt  6839  oprabv  7193  elovmporab  7371  elovmporab1w  7372  elovmporab1  7373  ovmpt3rabdm  7384  elovmpt3rab1  7385  tfindes  7557  findes  7593  dfopab2  7732  dfoprab3s  7733  mpoxopoveq  7868  findcard2  8742  ac6sfi  8746  indexfi  8816  nn0ind-raph  12070  uzind4s  12296  fzrevral  12987  rabssnn0fi  13349  prmind2  16019  elmptrab  22432  isfildlem  22462  2sqreulem4  26038  gropd  26824  grstructd  26825  rspc2daf  30238  opreu2reuALT  30247  bnj919  32148  bnj1468  32228  bnj110  32240  bnj607  32298  bnj873  32306  bnj849  32307  bnj1388  32415  bnj1489  32438  setinds  33136  dfon2lem1  33141  tfisg  33168  frpoinsg  33194  frinsg  33200  rdgssun  34795  indexa  35171  indexdom  35172  sdclem2  35180  sdclem1  35181  fdc1  35184  alrimii  35557  riotasv2s  36254  sbccomieg  39734  rexrabdioph  39735  rexfrabdioph  39736  aomclem6  40003  pm14.24  41136  or2expropbilem2  43625  or2expropbi  43626  ich2exprop  43988  ichnreuop  43989  ichreuopeq  43990  prproropreud  44026  reupr  44039  reuopreuprim  44043