Theorem nfsbc1v 3758

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

Syntax hints:  Ⅎwnf 1784  [wsbc 3738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-sbc 3739

This theorem is referenced by:  elrabsf  3784  cbvralcsf  3889  reusngf  4629  rexreusng  4634  reuprg0  4657  rmosn  4674  rabsnifsb  4677  euotd  5459  reuop  6249  frpoinsg  6299  elfvmptrab1w  6966  elfvmptrab1  6967  ralrnmptw  7037  ralrnmpt  7039  oprabv  7416  elovmporab  7602  elovmporab1w  7603  elovmporab1  7604  ovmpt3rabdm  7615  elovmpt3rab1  7616  tfisg  7794  tfindes  7803  findes  7840  dfopab2  7994  dfoprab3s  7995  ralxpes  8076  ralxp3es  8079  frpoins3xpg  8080  frpoins3xp3g  8081  mpoxopoveq  8159  findcard2  9087  ac6sfi  9182  indexfi  9258  setinds  9656  frinsg  9661  nn0ind-raph  12590  uzind4s  12819  fzrevral  13526  rabssnn0fi  13907  prmind2  16610  elmptrab  23769  isfildlem  23799  2sqreulem4  27419  gropd  29053  grstructd  29054  rspc2daf  32489  opreu2reuALT  32500  bnj919  34872  bnj1468  34951  bnj110  34963  bnj607  35021  bnj873  35029  bnj849  35030  bnj1388  35138  bnj1489  35161  dfon2lem1  35924  rdgssun  37522  indexa  37873  indexdom  37874  sdclem2  37882  sdclem1  37883  fdc1  37886  alrimii  38259  riotasv2s  39157  sbccomieg  42977  rexrabdioph  42978  rexfrabdioph  42979  aomclem6  43243  pm14.24  44615  or2expropbilem2  47221  or2expropbi  47222  ich2exprop  47659  ichnreuop  47660  ichreuopeq  47661  prproropreud  47697  reupr  47710  reuopreuprim  47714