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

Theorem nfsbc1v 3790
 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 2975 . 2 𝑥𝐴
21nfsbc1 3789 1 𝑥[𝐴 / 𝑥]𝜑
 Colors of variables: wff setvar class Syntax hints:  Ⅎwnf 1778  [wsbc 3770 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-sbc 3771 This theorem is referenced by:  elrabsf  3814  cbvralcsf  3923  vtocl2dOLD  3929  reusngf  4604  rexreusng  4609  reuprg0  4630  rmosn  4647  rabsnifsb  4650  euotd  5394  reuop  6137  wfisg  6176  elfvmptrab1w  6787  elfvmptrab1  6788  ralrnmptw  6853  ralrnmpt  6855  oprabv  7206  elovmporab  7383  elovmporab1w  7384  elovmporab1  7385  ovmpt3rabdm  7396  elovmpt3rab1  7397  tfindes  7569  findes  7604  dfopab2  7742  dfoprab3s  7743  mpoxopoveq  7877  findcard2  8750  ac6sfi  8754  indexfi  8824  nn0ind-raph  12074  uzind4s  12300  fzrevral  12984  rabssnn0fi  13346  prmind2  16021  elmptrab  22427  isfildlem  22457  2sqreulem4  26022  gropd  26808  grstructd  26809  rspc2daf  30223  opreu2reuALT  30232  bnj919  32031  bnj1468  32111  bnj110  32123  bnj607  32181  bnj873  32189  bnj849  32190  bnj1388  32298  bnj1489  32321  setinds  33016  dfon2lem1  33021  tfisg  33048  frpoinsg  33074  frinsg  33080  rdgssun  34651  indexa  35000  indexdom  35001  sdclem2  35009  sdclem1  35010  fdc1  35013  alrimii  35389  riotasv2s  36086  sbccomieg  39381  rexrabdioph  39382  rexfrabdioph  39383  aomclem6  39650  pm14.24  40755  or2expropbilem2  43259  or2expropbi  43260  ich2exprop  43624  ichnreuop  43625  ichreuopeq  43626  prproropreud  43662  reupr  43675  reuopreuprim  43679
 Copyright terms: Public domain W3C validator