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

Theorem nfsbc1v 3759
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 2907 . 2 𝑥𝐴
21nfsbc1 3758 1 𝑥[𝐴 / 𝑥]𝜑
Colors of variables: wff setvar class
Syntax hints:  wnf 1785  [wsbc 3739
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-sbc 3740
This theorem is referenced by:  elrabsf  3787  cbvralcsf  3900  reusngf  4633  rexreusng  4640  reuprg0  4663  rmosn  4680  rabsnifsb  4683  euotd  5470  reuop  6245  frpoinsg  6297  wfisgOLD  6308  elfvmptrab1w  6974  elfvmptrab1  6975  ralrnmptw  7043  ralrnmpt  7045  oprabv  7416  elovmporab  7598  elovmporab1w  7599  elovmporab1  7600  ovmpt3rabdm  7611  elovmpt3rab1  7612  tfisg  7789  tfindes  7798  findes  7838  dfopab2  7983  dfoprab3s  7984  ralxpes  8067  ralxp3es  8070  frpoins3xpg  8071  frpoins3xp3g  8072  mpoxopoveq  8149  findcard2  9107  findcard2OLD  9227  ac6sfi  9230  indexfi  9303  frinsg  9686  nn0ind-raph  12602  uzind4s  12832  fzrevral  13525  rabssnn0fi  13890  prmind2  16560  elmptrab  23176  isfildlem  23206  2sqreulem4  26800  gropd  27929  grstructd  27930  rspc2daf  31344  opreu2reuALT  31352  bnj919  33319  bnj1468  33398  bnj110  33410  bnj607  33468  bnj873  33476  bnj849  33477  bnj1388  33585  bnj1489  33608  setinds  34293  dfon2lem1  34298  rdgssun  35839  indexa  36182  indexdom  36183  sdclem2  36191  sdclem1  36192  fdc1  36195  alrimii  36568  riotasv2s  37410  sbccomieg  41093  rexrabdioph  41094  rexfrabdioph  41095  aomclem6  41363  pm14.24  42693  or2expropbilem2  45238  or2expropbi  45239  ich2exprop  45634  ichnreuop  45635  ichreuopeq  45636  prproropreud  45672  reupr  45685  reuopreuprim  45689
  Copyright terms: Public domain W3C validator