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

Theorem nfsbc1v 3488
Description: Bound-variable hypothesis builder for class substitution. (Contributed by Mario Carneiro, 12-Oct-2016.)
Assertion
Ref Expression
nfsbc1v 𝑥[𝐴 / 𝑥]𝜑
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem nfsbc1v
StepHypRef Expression
1 nfcv 2793 . 2 𝑥𝐴
21nfsbc1 3487 1 𝑥[𝐴 / 𝑥]𝜑
Colors of variables: wff setvar class
Syntax hints:  wnf 1748  [wsbc 3468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-sbc 3469
This theorem is referenced by:  elrabsf  3507  cbvralcsf  3598  rabsnifsb  4289  euotd  5004  wfisg  5753  elfvmptrab1  6344  ralrnmpt  6408  oprabv  6745  elovmpt2rab  6922  elovmpt2rab1  6923  ovmpt3rabdm  6934  elovmpt3rab1  6935  tfindes  7104  findes  7138  dfopab2  7266  dfoprab3s  7267  mpt2xopoveq  7390  findcard2  8241  ac6sfi  8245  indexfi  8315  nn0ind-raph  11515  uzind4s  11786  fzrevral  12463  rabssnn0fi  12825  prmind2  15445  elmptrab  21678  isfildlem  21708  gropd  25968  grstructd  25969  vtocl2d  29442  bnj919  30963  bnj1468  31042  bnj110  31054  bnj607  31112  bnj873  31120  bnj849  31121  bnj1388  31227  bnj1489  31250  setinds  31807  dfon2lem1  31812  tfisg  31840  frpoinsg  31866  frinsg  31870  indexa  33658  indexdom  33659  sdclem2  33668  sdclem1  33669  fdc1  33672  alrimii  34054  riotasv2s  34562  sbccomieg  37674  rexrabdioph  37675  rexfrabdioph  37676  aomclem6  37946  pm14.24  38950
  Copyright terms: Public domain W3C validator