Theorem nfsbc1v 3765

Description: Bound-variable hypothesis builder for class substitution. (Contributed by Mario Carneiro, 12-Oct-2016.)

Assertion

Ref	Expression
nfsbc1v	⊢ Ⅎ𝑥[𝐴 / 𝑥]𝜑

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem nfsbc1v

Step	Hyp	Ref	Expression
1		nfcv 2925	. 2 ⊢ Ⅎ𝑥𝐴
2	1	nfsbc1 3764	1 ⊢ Ⅎ𝑥[𝐴 / 𝑥]𝜑

Syntax hints:  Ⅎwnf 1804  [wsbc 3745

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1564  df-ex 1801  df-nf 1805  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-sbc 3746

This theorem is referenced by:  elrabsf  3790  cbvralcsf  3895  reusngf  4634  rexreusng  4639  reuprg0  4662  rmosn  4679  rabsnifsb  4682  euotd  5483  reuop  6281  frpoinsg  6331  elfvmptrab1w  7004  elfvmptrab1  7005  ralrnmptw  7076  ralrnmpt  7078  oprabv  7457  elovmporab  7643  elovmporab1w  7644  elovmporab1  7645  ovmpt3rabdm  7656  elovmpt3rab1  7657  tfisg  7835  tfindes  7844  findes  7882  dfopab2  8034  dfoprab3s  8035  ralxpes  8117  ralxp3es  8120  frpoins3xpg  8121  frpoins3xp3g  8122  mpoxopoveq  8200  findcard2  9134  ac6sfi  9229  indexfi  9304  setinds  9705  frinsg  9710  nn0ind-raph  12674  uzind4s  12910  fzrevral  13618  rabssnn0fi  14000  prmind2  16720  elmptrab  23888  isfildlem  23918  2sqreulem4  27519  gropd  29233  grstructd  29234  rspc2daf  32667  opreu2reuALT  32677  bnj919  35064  bnj1468  35142  bnj110  35154  bnj607  35212  bnj873  35220  bnj849  35221  bnj1388  35329  bnj1489  35352  dfon2lem1  36132  rdgssun  37873  indexa  38233  indexdom  38234  sdclem2  38242  sdclem1  38243  fdc1  38246  alrimii  38619  riotasv2s  39583  sbccomieg  43371  rexrabdioph  43372  rexfrabdioph  43373  aomclem6  43637  pm14.24  45009  or2expropbilem2  47628  or2expropbi  47629  ich2exprop  48078  ichnreuop  48079  ichreuopeq  48080  prproropreud  48116  reupr  48129  reuopreuprim  48133