Theorem nfsbc1v 3762

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

Syntax hints:  Ⅎwnf 1783  [wsbc 3742

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-sbc 3743

This theorem is referenced by:  elrabsf  3788  cbvralcsf  3893  reusngf  4626  rexreusng  4631  reuprg0  4654  rmosn  4671  rabsnifsb  4674  euotd  5456  reuop  6241  frpoinsg  6291  elfvmptrab1w  6957  elfvmptrab1  6958  ralrnmptw  7028  ralrnmpt  7030  oprabv  7409  elovmporab  7595  elovmporab1w  7596  elovmporab1  7597  ovmpt3rabdm  7608  elovmpt3rab1  7609  tfisg  7787  tfindes  7796  findes  7833  dfopab2  7987  dfoprab3s  7988  ralxpes  8069  ralxp3es  8072  frpoins3xpg  8073  frpoins3xp3g  8074  mpoxopoveq  8152  findcard2  9078  ac6sfi  9173  indexfi  9250  frinsg  9647  nn0ind-raph  12576  uzind4s  12809  fzrevral  13515  rabssnn0fi  13893  prmind2  16596  elmptrab  23712  isfildlem  23742  2sqreulem4  27363  gropd  28976  grstructd  28977  rspc2daf  32410  opreu2reuALT  32421  bnj919  34740  bnj1468  34819  bnj110  34831  bnj607  34889  bnj873  34897  bnj849  34898  bnj1388  35006  bnj1489  35029  setinds  35762  dfon2lem1  35767  rdgssun  37362  indexa  37723  indexdom  37724  sdclem2  37732  sdclem1  37733  fdc1  37736  alrimii  38109  riotasv2s  38947  sbccomieg  42776  rexrabdioph  42777  rexfrabdioph  42778  aomclem6  43042  pm14.24  44415  or2expropbilem2  47027  or2expropbi  47028  ich2exprop  47465  ichnreuop  47466  ichreuopeq  47467  prproropreud  47503  reupr  47516  reuopreuprim  47520