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

Theorem nfsbc1v 3319
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 2580 . 2  |-  F/_ x A
21nfsbc1 3318 1  |-  F/ x [. A  /  x ]. ph
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1661   [.wsbc 3299
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-sbc 3300
This theorem is referenced by:  elrabsf  3338  cbvralcsf  3427  rabsnifsb  4068  euotd  4721  wfisg  5434  elfvmptrab1  5986  ralrnmpt  6046  oprabv  6353  elovmpt2rab  6529  elovmpt2rab1  6530  ovmpt3rabdm  6540  elovmpt3rab1  6541  tfindes  6703  findes  6737  dfopab2  6861  dfoprab3s  6862  mpt2xopoveq  6976  findcard2  7820  ac6sfi  7824  indexfi  7891  nn0ind-raph  11042  uzind4s  11226  fzrevral  11886  rabssnn0fi  12204  prmind2  14634  elmptrab  20840  isfildlem  20870  vtocl2d  28107  bnj919  29586  bnj1468  29665  bnj110  29677  bnj607  29735  bnj873  29743  bnj849  29744  bnj1388  29850  bnj1489  29873  setinds  30431  dfon2lem1  30436  tfisg  30464  frinsg  30490  indexa  32024  indexdom  32025  sdclem2  32035  sdclem1  32036  fdc1  32039  alrimii  32323  riotasv2s  32499  sbccomieg  35605  rexrabdioph  35606  rexfrabdioph  35607  aomclem6  35887  pm14.24  36753  gropd  38963  grstructd  38964
  Copyright terms: Public domain W3C validator