Theorem nfsbc1v 3455

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

Syntax hints:   F/wnf 1708   [.wsbc 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-sbc 3436

This theorem is referenced by:  elrabsf  3474  cbvralcsf  3565  rabsnifsb  4257  euotd  4975  wfisg  5715  elfvmptrab1  6305  ralrnmpt  6368  oprabv  6703  elovmpt2rab  6880  elovmpt2rab1  6881  ovmpt3rabdm  6892  elovmpt3rab1  6893  tfindes  7062  findes  7096  dfopab2  7222  dfoprab3s  7223  mpt2xopoveq  7345  findcard2  8200  ac6sfi  8204  indexfi  8274  nn0ind-raph  11477  uzind4s  11748  fzrevral  12425  rabssnn0fi  12785  prmind2  15398  elmptrab  21630  isfildlem  21661  gropd  25923  grstructd  25924  vtocl2d  29314  bnj919  30837  bnj1468  30916  bnj110  30928  bnj607  30986  bnj873  30994  bnj849  30995  bnj1388  31101  bnj1489  31124  setinds  31683  dfon2lem1  31688  tfisg  31716  frinsg  31742  indexa  33528  indexdom  33529  sdclem2  33538  sdclem1  33539  fdc1  33542  alrimii  33924  riotasv2s  34244  sbccomieg  37357  rexrabdioph  37358  rexfrabdioph  37359  aomclem6  37629  pm14.24  38633