Theorem nfsbc1v 3422

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 2751	. 2 ⊢ Ⅎ𝑥𝐴
2	1	nfsbc1 3421	1 ⊢ Ⅎ𝑥[𝐴 / 𝑥]𝜑

Syntax hints:  Ⅎwnf 1699  [wsbc 3402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-sbc 3403

This theorem is referenced by:  elrabsf  3441  cbvralcsf  3531  rabsnifsb  4201  euotd  4900  wfisg  5632  elfvmptrab1  6213  ralrnmpt  6276  oprabv  6601  elovmpt2rab  6778  elovmpt2rab1  6779  ovmpt3rabdm  6790  elovmpt3rab1  6791  tfindes  6954  findes  6988  dfopab2  7113  dfoprab3s  7114  mpt2xopoveq  7232  findcard2  8085  ac6sfi  8089  indexfi  8157  nn0ind-raph  11353  uzind4s  11624  fzrevral  12294  rabssnn0fi  12647  prmind2  15236  elmptrab  21440  isfildlem  21471  gropd  25708  grstructd  25709  vtocl2d  28699  bnj919  30091  bnj1468  30170  bnj110  30182  bnj607  30240  bnj873  30248  bnj849  30249  bnj1388  30355  bnj1489  30378  setinds  30927  dfon2lem1  30932  tfisg  30960  frinsg  30986  indexa  32698  indexdom  32699  sdclem2  32708  sdclem1  32709  fdc1  32712  alrimii  33094  riotasv2s  33262  sbccomieg  36375  rexrabdioph  36376  rexfrabdioph  36377  aomclem6  36647  pm14.24  37655