Theorem nfsbc1v 3325

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

Syntax hints:   F/wnf 1663   [.wsbc 3305

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-sbc 3306

This theorem is referenced by:  elrabsf  3344  cbvralcsf  3433  rabsnifsb  4071  euotd  4722  wfisg  5434  elfvmptrab1  5986  ralrnmpt  6046  oprabv  6353  elovmpt2rab  6529  elovmpt2rab1  6530  ovmpt3rabdm  6540  elovmpt3rab1  6541  tfindes  6703  findes  6737  dfopab2  6861  dfoprab3s  6862  mpt2xopoveq  6973  findcard2  7817  ac6sfi  7821  indexfi  7888  nn0ind-raph  11035  uzind4s  11219  fzrevral  11877  rabssnn0fi  12195  prmind2  14606  elmptrab  20773  isfildlem  20803  vtocl2d  27944  bnj919  29366  bnj1468  29445  bnj110  29457  bnj607  29515  bnj873  29523  bnj849  29524  bnj1388  29630  bnj1489  29653  setinds  30211  dfon2lem1  30216  tfisg  30244  frinsg  30270  indexa  31763  indexdom  31764  sdclem2  31774  sdclem1  31775  fdc1  31778  alrimii  32062  riotasv2s  32238  sbccomieg  35344  rexrabdioph  35345  rexfrabdioph  35346  aomclem6  35622  pm14.24  36419