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

Theorem nfsbc1v 3023
Description: Bound-variable hypothesis builder for class substitution. (Contributed by Mario Carneiro, 12-Oct-2016.)
Assertion
Ref Expression
nfsbc1v  |-  F/ x [. A  /  x ]. ph
Distinct variable group:    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem nfsbc1v
StepHypRef Expression
1 nfcv 2432 . 2  |-  F/_ x A
21nfsbc1 3022 1  |-  F/ x [. A  /  x ]. ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1534   [.wsbc 3004
This theorem is referenced by:  elrabsf  3042  cbvralcsf  3156  euotd  4283  tfindes  4669  findes  4702  ralrnmpt  5685  dfopab2  6190  dfoprab3s  6191  riotasv2s  6367  findcard2  7114  ac6sfi  7117  indexfi  7179  uzindOLD  10122  nn0ind-raph  10128  uzind4s  10294  fzrevral  10882  prmind2  12785  elmptrab  17538  isfildlem  17568  setinds  24205  dfon2lem1  24210  tfisg  24275  wfisg  24280  frinsg  24316  indexa  26515  indexdom  26516  sdclem2  26555  sdclem1  26556  fdc1  26559  sbccomieg  26973  rexrabdioph  26978  rexfrabdioph  26979  aomclem6  27259  pm14.24  27735  mpt2xopoveq  28201  bnj919  29113  bnj1468  29194  bnj110  29206  bnj607  29264  bnj849  29273  bnj1388  29379  bnj1489  29402
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-sbc 3005
  Copyright terms: Public domain W3C validator