Theorem nfsbc1v 3272

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

Syntax hints:   F/wnf 1624   [.wsbc 3252

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-sbc 3253

This theorem is referenced by:  elrabsf  3291  cbvralcsf  3380  rabsnifsb  4012  euotd  4662  elfvmptrab1  5878  ralrnmpt  5942  oprabv  6244  elovmpt2rab  6420  elovmpt2rab1  6421  ovmpt3rabdm  6434  elovmpt3rab1  6435  tfindes  6596  findes  6629  dfopab2  6753  dfoprab3s  6754  mpt2xopoveq  6865  findcard2  7675  ac6sfi  7679  indexfi  7743  nn0ind-raph  10879  uzind4s  11061  fzrevral  11685  rabssnn0fi  11998  prmind2  14230  elmptrab  20413  isfildlem  20443  setinds  29375  dfon2lem1  29380  tfisg  29449  wfisg  29454  frinsg  29490  indexa  30390  indexdom  30391  sdclem2  30401  sdclem1  30402  fdc1  30405  alrimii  30690  sbccomieg  30892  rexrabdioph  30893  rexfrabdioph  30894  aomclem6  31171  pm14.24  31507  bnj919  34172  bnj1468  34251  bnj110  34263  bnj607  34321  bnj873  34329  bnj849  34330  bnj1388  34436  bnj1489  34459  riotasv2s  35102