Theorem nfsbc1v 3306

Description: Bound-variable hypothesis builder for class substitution. (Contributed by Mario Carneiro, 12-Oct-2016.)

Assertion

Ref	Expression
nfsbc1v	|- F/ x [. A / x ]. ph

Distinct variable group:   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem nfsbc1v

Step	Hyp	Ref	Expression
1		nfcv 2613	. 2 |- F/_ x A
2	1	nfsbc1 3305	1 |- F/ x [. A / x ]. ph

Syntax hints:   F/wnf 1590   [.wsbc 3286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-sbc 3287

This theorem is referenced by:  elrabsf  3325  cbvralcsf  3419  rabsnifsb  4043  euotd  4692  ralrnmpt  5953  tfindes  6575  findes  6608  dfopab2  6730  dfoprab3s  6731  mpt2xopoveq  6838  findcard2  7655  ac6sfi  7659  indexfi  7722  uzindOLD  10839  nn0ind-raph  10845  uzind4s  11017  fzrevral  11647  prmind2  13878  elmptrab  19518  isfildlem  19548  setinds  27727  dfon2lem1  27732  tfisg  27801  wfisg  27806  frinsg  27842  indexa  28767  indexdom  28768  sdclem2  28778  sdclem1  28779  fdc1  28782  alrimii  29067  sbccomieg  29271  rexrabdioph  29272  rexfrabdioph  29273  aomclem6  29552  pm14.24  29826  elfvmptrab1  30294  oprabv  30297  elovmpt2rab  30298  elovmpt2rab1  30299  elovmpt3rab1  30303  rabssnn0fi  30887  bnj919  32062  bnj1468  32141  bnj110  32153  bnj607  32211  bnj873  32219  bnj849  32220  bnj1388  32326  bnj1489  32349  riotasv2s  32917