Theorem nfsbc1v 3299

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

Syntax hints:   F/wnf 1678   [.wsbc 3279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-sbc 3280

This theorem is referenced by:  elrabsf  3318  cbvralcsf  3407  rabsnifsb  4053  euotd  4719  wfisg  5438  elfvmptrab1  5998  ralrnmpt  6059  oprabv  6371  elovmpt2rab  6547  elovmpt2rab1  6548  ovmpt3rabdm  6558  elovmpt3rab1  6559  tfindes  6721  findes  6755  dfopab2  6879  dfoprab3s  6880  mpt2xopoveq  6997  findcard2  7842  ac6sfi  7846  indexfi  7913  nn0ind-raph  11069  uzind4s  11253  fzrevral  11914  rabssnn0fi  12236  prmind2  14690  elmptrab  20897  isfildlem  20927  vtocl2d  28165  bnj919  29628  bnj1468  29707  bnj110  29719  bnj607  29777  bnj873  29785  bnj849  29786  bnj1388  29892  bnj1489  29915  setinds  30474  dfon2lem1  30479  tfisg  30507  frinsg  30533  indexa  32106  indexdom  32107  sdclem2  32117  sdclem1  32118  fdc1  32121  alrimii  32405  riotasv2s  32576  sbccomieg  35682  rexrabdioph  35683  rexfrabdioph  35684  aomclem6  35963  pm14.24  36828  gropd  39275  grstructd  39276