Theorem nfsbc1v 3764

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

This proof depends on syntax axioms:  Ⅎwnf 1813  [wsbc 3744

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-sbc 3745

This theorem is used by:  elrabsf  3789  cbvralcsf  3895  reusngf  4640  rexreusng  4645  reuprg0  4668  rmosn  4685  rabsnifsb  4688  euotd  5496  reuop  6294  frpoinsg  6344  elfvmptrab1w  7017  elfvmptrab1  7018  ralrnmptw  7089  ralrnmpt  7091  oprabv  7470  elovmporab  7656  elovmporab1w  7657  elovmporab1  7658  ovmpt3rabdm  7669  elovmpt3rab1  7670  tfisg  7846  tfindes  7855  findes  7893  dfopab2  8045  dfoprab3s  8046  ralxpes  8128  ralxp3es  8131  frpoins3xpg  8132  frpoins3xp3g  8133  mpoxopoveq  8211  findcard2  9145  ac6sfi  9240  indexfi  9313  setinds  9714  frinsg  9719  nn0ind-raph  12700  uzind4s  12936  fzrevral  13645  rabssnn0fi  14027  prmind2  16747  elmptrab  23993  isfildlem  24023  2sqreulem4  27627  gropd  29390  grstructd  29391  rspc2daf  32822  opreu2reuALT  32832  bnj919  35165  bnj1468  35243  bnj110  35255  bnj607  35313  bnj873  35321  bnj849  35322  bnj1388  35430  bnj1489  35453  dfon2lem1  36281  rdgssun  38052  indexa  38412  indexdom  38413  sdclem2  38421  sdclem1  38422  fdc1  38425  alrimii  38796  riotasv2s  39760  sbccomieg  43548  rexrabdioph  43549  rexfrabdioph  43550  aomclem6  43814  pm14.24  45170  or2expropbilem2  47798  or2expropbi  47799  ich2exprop  48248  ichnreuop  48249  ichreuopeq  48250  prproropreud  48286  reupr  48299  reuopreuprim  48303