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

Theorem nfsbc1v 3347
Description: Bound-variable hypothesis builder for class substitution. (Contributed by Mario Carneiro, 12-Oct-2016.)
Assertion
Ref Expression
nfsbc1v
Distinct variable group:   ,

Proof of Theorem nfsbc1v
StepHypRef Expression
1 nfcv 2619 . 2
21nfsbc1 3346 1
Colors of variables: wff setvar class
Syntax hints:  F/wnf 1616  [.wsbc 3327
This theorem is referenced by:  elrabsf  3366  cbvralcsf  3466  rabsnifsb  4098  euotd  4753  elfvmptrab1  5976  ralrnmpt  6040  oprabv  6345  elovmpt2rab  6521  elovmpt2rab1  6522  ovmpt3rabdm  6535  elovmpt3rab1  6536  tfindes  6697  findes  6730  dfopab2  6854  dfoprab3s  6855  mpt2xopoveq  6966  findcard2  7780  ac6sfi  7784  indexfi  7848  uzindOLD  10982  nn0ind-raph  10989  uzind4s  11170  fzrevral  11792  rabssnn0fi  12095  prmind2  14228  elmptrab  20328  isfildlem  20358  setinds  29210  dfon2lem1  29215  tfisg  29284  wfisg  29289  frinsg  29325  indexa  30224  indexdom  30225  sdclem2  30235  sdclem1  30236  fdc1  30239  alrimii  30524  sbccomieg  30726  rexrabdioph  30727  rexfrabdioph  30728  aomclem6  31005  pm14.24  31339  bnj919  33825  bnj1468  33904  bnj110  33916  bnj607  33974  bnj873  33982  bnj849  33983  bnj1388  34089  bnj1489  34112  riotasv2s  34689
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-sbc 3328
  Copyright terms: Public domain W3C validator