Theorem nfsbc1v 3759

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

This proof depends on syntax axioms:  Ⅎwnf 1816  [wsbc 3739

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-sbc 3740

This theorem is used by:  elrabsf  3784  cbvralcsf  3889  reusngf  4635  rexreusng  4640  reuprg0  4663  rmosn  4680  rabsnifsb  4683  euotd  5490  reuop  6291  frpoinsg  6341  elfvmptrab1w  7015  elfvmptrab1  7016  ralrnmptw  7088  ralrnmpt  7090  oprabv  7474  elovmporab  7661  elovmporab1w  7662  elovmporab1  7663  ovmpt3rabdm  7674  elovmpt3rab1  7675  tfisg  7851  tfindes  7860  findes  7898  dfopab2  8050  dfoprab3s  8051  ralxpes  8135  ralxp3es  8138  frpoins3xpg  8139  frpoins3xp3g  8140  mpoxopoveq  8218  findcard2  9162  ac6sfi  9257  indexfi  9330  setinds  9731  frinsg  9736  nn0ind-raph  12724  uzind4s  12960  fzrevral  13670  rabssnn0fi  14053  prmind2  16778  elmptrab  24056  isfildlem  24086  2sqreulem4  27693  gropd  29491  grstructd  29492  rspc2daf  32945  opreu2reuALT  32955  bnj919  35280  bnj1468  35358  bnj110  35370  bnj607  35428  bnj873  35436  bnj849  35437  bnj1388  35545  bnj1489  35568  dfon2lem1  36363  rdgssun  38135  indexa  38486  indexdom  38487  sdclem2  38495  sdclem1  38496  fdc1  38499  alrimii  38870  riotasv2s  39834  sbccomieg  43637  rexrabdioph  43638  rexfrabdioph  43639  aomclem6  43903  pm14.24  45259  or2expropbilem2  47924  or2expropbi  47925  ich2exprop  48374  ichnreuop  48375  ichreuopeq  48376  prproropreud  48412  reupr  48425  reuopreuprim  48429