Theorem nfsbc1v 3333

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

Syntax hints:   F/wnf 1603   [.wsbc 3313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-sbc 3314

This theorem is referenced by:  elrabsf  3352  cbvralcsf  3452  rabsnifsb  4083  euotd  4738  elfvmptrab1  5961  ralrnmpt  6025  oprabv  6330  elovmpt2rab  6506  elovmpt2rab1  6507  ovmpt3rabdm  6520  elovmpt3rab1  6521  tfindes  6682  findes  6715  dfopab2  6839  dfoprab3s  6840  mpt2xopoveq  6949  findcard2  7762  ac6sfi  7766  indexfi  7830  uzindOLD  10963  nn0ind-raph  10969  uzind4s  11150  fzrevral  11771  rabssnn0fi  12074  prmind2  14105  elmptrab  20201  isfildlem  20231  setinds  29185  dfon2lem1  29190  tfisg  29259  wfisg  29264  frinsg  29300  indexa  30199  indexdom  30200  sdclem2  30210  sdclem1  30211  fdc1  30214  alrimii  30499  sbccomieg  30701  rexrabdioph  30702  rexfrabdioph  30703  aomclem6  30980  pm14.24  31293  bnj919  33558  bnj1468  33637  bnj110  33649  bnj607  33707  bnj873  33715  bnj849  33716  bnj1388  33822  bnj1489  33845  riotasv2s  34429