Theorem nfsbc1v 3736

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

Syntax hints:  Ⅎwnf 1786  [wsbc 3716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-sbc 3717

This theorem is referenced by:  elrabsf  3764  cbvralcsf  3877  reusngf  4608  rexreusng  4615  reuprg0  4638  rmosn  4655  rabsnifsb  4658  euotd  5427  reuop  6196  frpoinsg  6246  wfisgOLD  6257  elfvmptrab1w  6901  elfvmptrab1  6902  ralrnmptw  6970  ralrnmpt  6972  oprabv  7335  elovmporab  7515  elovmporab1w  7516  elovmporab1  7517  ovmpt3rabdm  7528  elovmpt3rab1  7529  tfindes  7709  findes  7749  dfopab2  7892  dfoprab3s  7893  mpoxopoveq  8035  findcard2  8947  findcard2OLD  9056  ac6sfi  9058  indexfi  9127  frinsg  9509  nn0ind-raph  12420  uzind4s  12648  fzrevral  13341  rabssnn0fi  13706  prmind2  16390  elmptrab  22978  isfildlem  23008  2sqreulem4  26602  gropd  27401  grstructd  27402  rspc2daf  30816  opreu2reuALT  30825  bnj919  32747  bnj1468  32826  bnj110  32838  bnj607  32896  bnj873  32904  bnj849  32905  bnj1388  33013  bnj1489  33036  ralxpes  33678  ralxp3es  33688  setinds  33754  dfon2lem1  33759  tfisg  33786  frpoins3xpg  33787  frpoins3xp3g  33788  rdgssun  35549  indexa  35891  indexdom  35892  sdclem2  35900  sdclem1  35901  fdc1  35904  alrimii  36277  riotasv2s  36972  sbccomieg  40615  rexrabdioph  40616  rexfrabdioph  40617  aomclem6  40884  pm14.24  42050  or2expropbilem2  44527  or2expropbi  44528  ich2exprop  44923  ichnreuop  44924  ichreuopeq  44925  prproropreud  44961  reupr  44974  reuopreuprim  44978