Theorem nfsbc1v 3790

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

Syntax hints:  Ⅎwnf 1783  [wsbc 3770

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-sbc 3771

This theorem is referenced by:  elrabsf  3816  cbvralcsf  3921  reusngf  4655  rexreusng  4660  reuprg0  4683  rmosn  4700  rabsnifsb  4703  euotd  5493  reuop  6287  frpoinsg  6337  wfisgOLD  6348  elfvmptrab1w  7018  elfvmptrab1  7019  ralrnmptw  7089  ralrnmpt  7091  oprabv  7472  elovmporab  7658  elovmporab1w  7659  elovmporab1  7660  ovmpt3rabdm  7671  elovmpt3rab1  7672  tfisg  7854  tfindes  7863  findes  7901  dfopab2  8056  dfoprab3s  8057  ralxpes  8140  ralxp3es  8143  frpoins3xpg  8144  frpoins3xp3g  8145  mpoxopoveq  8223  findcard2  9183  ac6sfi  9297  indexfi  9377  frinsg  9770  nn0ind-raph  12698  uzind4s  12929  fzrevral  13634  rabssnn0fi  14009  prmind2  16709  elmptrab  23770  isfildlem  23800  2sqreulem4  27422  gropd  29015  grstructd  29016  rspc2daf  32452  opreu2reuALT  32463  bnj919  34803  bnj1468  34882  bnj110  34894  bnj607  34952  bnj873  34960  bnj849  34961  bnj1388  35069  bnj1489  35092  setinds  35801  dfon2lem1  35806  rdgssun  37401  indexa  37762  indexdom  37763  sdclem2  37771  sdclem1  37772  fdc1  37775  alrimii  38148  riotasv2s  38981  sbccomieg  42791  rexrabdioph  42792  rexfrabdioph  42793  aomclem6  43058  pm14.24  44431  or2expropbilem2  47042  or2expropbi  47043  ich2exprop  47465  ichnreuop  47466  ichreuopeq  47467  prproropreud  47503  reupr  47516  reuopreuprim  47520