Theorem nfsbc1v 3775

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

Syntax hints:  Ⅎwnf 1783  [wsbc 3755

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-sbc 3756

This theorem is referenced by:  elrabsf  3801  cbvralcsf  3906  reusngf  4640  rexreusng  4645  reuprg0  4668  rmosn  4685  rabsnifsb  4688  euotd  5475  reuop  6268  frpoinsg  6318  elfvmptrab1w  6997  elfvmptrab1  6998  ralrnmptw  7068  ralrnmpt  7070  oprabv  7451  elovmporab  7637  elovmporab1w  7638  elovmporab1  7639  ovmpt3rabdm  7650  elovmpt3rab1  7651  tfisg  7832  tfindes  7841  findes  7878  dfopab2  8033  dfoprab3s  8034  ralxpes  8117  ralxp3es  8120  frpoins3xpg  8121  frpoins3xp3g  8122  mpoxopoveq  8200  findcard2  9133  ac6sfi  9237  indexfi  9317  frinsg  9710  nn0ind-raph  12640  uzind4s  12873  fzrevral  13579  rabssnn0fi  13957  prmind2  16661  elmptrab  23720  isfildlem  23750  2sqreulem4  27371  gropd  28964  grstructd  28965  rspc2daf  32401  opreu2reuALT  32412  bnj919  34763  bnj1468  34842  bnj110  34854  bnj607  34912  bnj873  34920  bnj849  34921  bnj1388  35029  bnj1489  35052  setinds  35761  dfon2lem1  35766  rdgssun  37361  indexa  37722  indexdom  37723  sdclem2  37731  sdclem1  37732  fdc1  37735  alrimii  38108  riotasv2s  38946  sbccomieg  42774  rexrabdioph  42775  rexfrabdioph  42776  aomclem6  43041  pm14.24  44414  or2expropbilem2  47024  or2expropbi  47025  ich2exprop  47462  ichnreuop  47463  ichreuopeq  47464  prproropreud  47500  reupr  47513  reuopreuprim  47517