MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfsbc1v Structured version   Visualization version   GIF version

Theorem nfsbc1v 3789
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
StepHypRef Expression
1 nfcv 2974 . 2 𝑥𝐴
21nfsbc1 3788 1 𝑥[𝐴 / 𝑥]𝜑
Colors of variables: wff setvar class
Syntax hints:  wnf 1775  [wsbc 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-sbc 3770
This theorem is referenced by:  elrabsf  3813  cbvralcsf  3922  vtocl2dOLD  3928  reusngf  4604  rexreusng  4609  reuprg0  4630  rmosn  4647  rabsnifsb  4650  euotd  5394  reuop  6137  wfisg  6176  elfvmptrab1w  6786  elfvmptrab1  6787  ralrnmptw  6852  ralrnmpt  6854  oprabv  7203  elovmporab  7380  elovmporab1w  7381  elovmporab1  7382  ovmpt3rabdm  7393  elovmpt3rab1  7394  tfindes  7566  findes  7601  dfopab2  7739  dfoprab3s  7740  mpoxopoveq  7874  findcard2  8746  ac6sfi  8750  indexfi  8820  nn0ind-raph  12070  uzind4s  12296  fzrevral  12980  rabssnn0fi  13342  prmind2  16017  elmptrab  22363  isfildlem  22393  2sqreulem4  25957  gropd  26743  grstructd  26744  rspc2daf  30158  opreu2reuALT  30167  bnj919  31937  bnj1468  32017  bnj110  32029  bnj607  32087  bnj873  32095  bnj849  32096  bnj1388  32202  bnj1489  32225  setinds  32920  dfon2lem1  32925  tfisg  32952  frpoinsg  32978  frinsg  32984  rdgssun  34541  indexa  34889  indexdom  34890  sdclem2  34898  sdclem1  34899  fdc1  34902  alrimii  35278  riotasv2s  35974  sbccomieg  39268  rexrabdioph  39269  rexfrabdioph  39270  aomclem6  39537  pm14.24  40641  or2expropbilem2  43145  or2expropbi  43146  ich2exprop  43510  ichnreuop  43511  ichreuopeq  43512  prproropreud  43548  reupr  43561  reuopreuprim  43565
  Copyright terms: Public domain W3C validator