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

Theorem nfsbc1v 3449
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 2762 . 2 𝑥𝐴
21nfsbc1 3448 1 𝑥[𝐴 / 𝑥]𝜑
Colors of variables: wff setvar class
Syntax hints:  wnf 1706  [wsbc 3429
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-sbc 3430
This theorem is referenced by:  elrabsf  3468  cbvralcsf  3558  rabsnifsb  4248  euotd  4965  wfisg  5703  elfvmptrab1  6291  ralrnmpt  6354  oprabv  6688  elovmpt2rab  6865  elovmpt2rab1  6866  ovmpt3rabdm  6877  elovmpt3rab1  6878  tfindes  7047  findes  7081  dfopab2  7207  dfoprab3s  7208  mpt2xopoveq  7330  findcard2  8185  ac6sfi  8189  indexfi  8259  nn0ind-raph  11462  uzind4s  11733  fzrevral  12409  rabssnn0fi  12768  prmind2  15379  elmptrab  21611  isfildlem  21642  gropd  25904  grstructd  25905  vtocl2d  29285  bnj919  30811  bnj1468  30890  bnj110  30902  bnj607  30960  bnj873  30968  bnj849  30969  bnj1388  31075  bnj1489  31098  setinds  31657  dfon2lem1  31662  tfisg  31690  frinsg  31716  indexa  33499  indexdom  33500  sdclem2  33509  sdclem1  33510  fdc1  33513  alrimii  33895  riotasv2s  34063  sbccomieg  37176  rexrabdioph  37177  rexfrabdioph  37178  aomclem6  37448  pm14.24  38453
  Copyright terms: Public domain W3C validator