Theorem nfsbc1v 3344

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 2622	. 2 |- F/_ x A
2	1	nfsbc1 3343	1 |- F/ x [. A / x ]. ph

Syntax hints:   F/wnf 1594   [.wsbc 3324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-sbc 3325

This theorem is referenced by:  elrabsf  3363  cbvralcsf  3460  rabsnifsb  4088  euotd  4741  elfvmptrab1  5961  ralrnmpt  6021  oprabv  6320  elovmpt2rab  6496  elovmpt2rab1  6497  elovmpt3rab1  6511  tfindes  6668  findes  6701  dfopab2  6828  dfoprab3s  6829  mpt2xopoveq  6937  findcard2  7749  ac6sfi  7753  indexfi  7817  uzindOLD  10944  nn0ind-raph  10950  uzind4s  11130  fzrevral  11751  rabssnn0fi  12051  prmind2  14076  elmptrab  20056  isfildlem  20086  setinds  28773  dfon2lem1  28778  tfisg  28847  wfisg  28852  frinsg  28888  indexa  29814  indexdom  29815  sdclem2  29825  sdclem1  29826  fdc1  29829  alrimii  30114  sbccomieg  30317  rexrabdioph  30318  rexfrabdioph  30319  aomclem6  30598  pm14.24  30872  bnj919  32779  bnj1468  32858  bnj110  32870  bnj607  32928  bnj873  32936  bnj849  32937  bnj1388  33043  bnj1489  33066  riotasv2s  33636