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

Theorem nfsbc1v 3182
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 2574 . 2  |-  F/_ x A
21nfsbc1 3181 1  |-  F/ x [. A  /  x ]. ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1554   [.wsbc 3163
This theorem is referenced by:  elrabsf  3201  cbvralcsf  3313  euotd  4459  tfindes  4844  findes  4877  ralrnmpt  5880  dfopab2  6403  dfoprab3s  6404  mpt2xopoveq  6472  riotasv2s  6598  findcard2  7350  ac6sfi  7353  indexfi  7416  uzindOLD  10366  nn0ind-raph  10372  uzind4s  10538  fzrevral  11133  prmind2  13092  elmptrab  17861  isfildlem  17891  setinds  25407  dfon2lem1  25412  tfisg  25481  wfisg  25486  frinsg  25522  indexa  26437  indexdom  26438  sdclem2  26448  sdclem1  26449  fdc1  26452  sbccomieg  26851  rexrabdioph  26856  rexfrabdioph  26857  aomclem6  27136  pm14.24  27611  oprabv  28091  elovmpt2rab  28092  elovmpt2rab1  28093  ovmpt3rab1  28094  elovmpt3rab1  28095  bnj919  29198  bnj1468  29279  bnj110  29291  bnj607  29349  bnj873  29357  bnj849  29358  bnj1388  29464  bnj1489  29487
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-sbc 3164
  Copyright terms: Public domain W3C validator