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

Theorem nfsbc1v 3607
 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 2913 . 2 𝑥𝐴
21nfsbc1 3606 1 𝑥[𝐴 / 𝑥]𝜑
 Colors of variables: wff setvar class Syntax hints:  Ⅎwnf 1856  [wsbc 3587 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-sbc 3588 This theorem is referenced by:  elrabsf  3626  cbvralcsf  3714  rabsnifsb  4393  euotd  5106  wfisg  5858  elfvmptrab1  6447  ralrnmpt  6511  oprabv  6850  elovmpt2rab  7027  elovmpt2rab1  7028  ovmpt3rabdm  7039  elovmpt3rab1  7040  tfindes  7209  findes  7243  dfopab2  7371  dfoprab3s  7372  mpt2xopoveq  7497  findcard2  8356  ac6sfi  8360  indexfi  8430  nn0ind-raph  11679  uzind4s  11950  fzrevral  12632  rabssnn0fi  12993  prmind2  15605  elmptrab  21851  isfildlem  21881  gropd  26144  grstructd  26145  vtocl2d  29654  bnj919  31175  bnj1468  31254  bnj110  31266  bnj607  31324  bnj873  31332  bnj849  31333  bnj1388  31439  bnj1489  31462  setinds  32019  dfon2lem1  32024  tfisg  32052  frpoinsg  32078  frinsg  32082  indexa  33860  indexdom  33861  sdclem2  33870  sdclem1  33871  fdc1  33874  alrimii  34256  riotasv2s  34766  sbccomieg  37883  rexrabdioph  37884  rexfrabdioph  37885  aomclem6  38155  pm14.24  39159
 Copyright terms: Public domain W3C validator