Theorem nfsbc1v 3766

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

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

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-sbc 3747

This theorem is used by:  elrabsf  3791  cbvralcsf  3896  reusngf  4642  rexreusng  4647  reuprg0  4670  rmosn  4687  rabsnifsb  4690  euotd  5498  reuop  6298  frpoinsg  6348  elfvmptrab1w  7021  elfvmptrab1  7022  ralrnmptw  7093  ralrnmpt  7095  oprabv  7479  elovmporab  7666  elovmporab1w  7667  elovmporab1  7668  ovmpt3rabdm  7679  elovmpt3rab1  7680  tfisg  7856  tfindes  7865  findes  7903  dfopab2  8055  dfoprab3s  8056  ralxpes  8138  ralxp3es  8141  frpoins3xpg  8142  frpoins3xp3g  8143  mpoxopoveq  8221  findcard2  9156  ac6sfi  9251  indexfi  9324  setinds  9725  frinsg  9730  nn0ind-raph  12716  uzind4s  12952  fzrevral  13661  rabssnn0fi  14044  prmind2  16769  elmptrab  24039  isfildlem  24069  2sqreulem4  27673  gropd  29440  grstructd  29441  rspc2daf  32888  opreu2reuALT  32898  bnj919  35225  bnj1468  35303  bnj110  35315  bnj607  35373  bnj873  35381  bnj849  35382  bnj1388  35490  bnj1489  35513  dfon2lem1  36314  rdgssun  38085  indexa  38446  indexdom  38447  sdclem2  38455  sdclem1  38456  fdc1  38459  alrimii  38830  riotasv2s  39794  sbccomieg  43597  rexrabdioph  43598  rexfrabdioph  43599  aomclem6  43863  pm14.24  45219  or2expropbilem2  47847  or2expropbi  47848  ich2exprop  48297  ichnreuop  48298  ichreuopeq  48299  prproropreud  48335  reupr  48348  reuopreuprim  48352