Theorem nfsbc1v 3792

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

Syntax hints:  Ⅎwnf 1782  [wsbc 3772

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-sbc 3773

This theorem is referenced by:  elrabsf  3818  cbvralcsf  3923  reusngf  4656  rexreusng  4661  reuprg0  4684  rmosn  4701  rabsnifsb  4704  euotd  5500  reuop  6295  frpoinsg  6345  wfisgOLD  6356  elfvmptrab1w  7024  elfvmptrab1  7025  ralrnmptw  7095  ralrnmpt  7097  oprabv  7476  elovmporab  7662  elovmporab1w  7663  elovmporab1  7664  ovmpt3rabdm  7675  elovmpt3rab1  7676  tfisg  7858  tfindes  7867  findes  7905  dfopab2  8060  dfoprab3s  8061  ralxpes  8144  ralxp3es  8147  frpoins3xpg  8148  frpoins3xp3g  8149  mpoxopoveq  8227  findcard2  9187  ac6sfi  9303  indexfi  9383  frinsg  9774  nn0ind-raph  12702  uzind4s  12933  fzrevral  13635  rabssnn0fi  14010  prmind2  16705  elmptrab  23800  isfildlem  23830  2sqreulem4  27453  gropd  28995  grstructd  28996  rspc2daf  32432  opreu2reuALT  32443  bnj919  34722  bnj1468  34801  bnj110  34813  bnj607  34871  bnj873  34879  bnj849  34880  bnj1388  34988  bnj1489  35011  setinds  35720  dfon2lem1  35725  rdgssun  37320  indexa  37681  indexdom  37682  sdclem2  37690  sdclem1  37691  fdc1  37694  alrimii  38067  riotasv2s  38900  sbccomieg  42749  rexrabdioph  42750  rexfrabdioph  42751  aomclem6  43016  pm14.24  44396  or2expropbilem2  46991  or2expropbi  46992  ich2exprop  47404  ichnreuop  47405  ichreuopeq  47406  prproropreud  47442  reupr  47455  reuopreuprim  47459