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

Theorem nfsbc1v 3010
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 2419 . 2  |-  F/_ x A
21nfsbc1 3009 1  |-  F/ x [. A  /  x ]. ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1531   [.wsbc 2991
This theorem is referenced by:  elrabsf  3029  cbvralcsf  3143  euotd  4267  tfindes  4653  findes  4686  ralrnmpt  5669  dfopab2  6174  dfoprab3s  6175  riotasv2s  6351  findcard2  7098  ac6sfi  7101  indexfi  7163  uzindOLD  10106  nn0ind-raph  10112  uzind4s  10278  fzrevral  10866  prmind2  12769  elmptrab  17522  isfildlem  17552  setinds  24134  dfon2lem1  24139  tfisg  24204  wfisg  24209  frinsg  24245  indexa  26412  indexdom  26413  sdclem2  26452  sdclem1  26453  fdc1  26456  sbccomieg  26870  rexrabdioph  26875  rexfrabdioph  26876  aomclem6  27156  pm14.24  27632  mpt2xopoveq  28085  bnj919  28797  bnj1468  28878  bnj110  28890  bnj607  28948  bnj849  28957  bnj1388  29063  bnj1489  29086
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-sbc 2992
  Copyright terms: Public domain W3C validator