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

Theorem nfcsb1 3922
Description: Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
Hypothesis
Ref Expression
nfcsb1.1 𝑥𝐴
Assertion
Ref Expression
nfcsb1 𝑥𝐴 / 𝑥𝐵

Proof of Theorem nfcsb1
StepHypRef Expression
1 nfcsb1.1 . . . 4 𝑥𝐴
21a1i 11 . . 3 (⊤ → 𝑥𝐴)
32nfcsb1d 3921 . 2 (⊤ → 𝑥𝐴 / 𝑥𝐵)
43mptru 1547 1 𝑥𝐴 / 𝑥𝐵
Colors of variables: wff setvar class
Syntax hints:  wtru 1541  wnfc 2890  csb 3899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-sbc 3789  df-csb 3900
This theorem is referenced by:  nfcsb1v  3923  fsumsplit1  15781  iundisj  25583  disjabrex  32595  disjabrexf  32596  iundisjf  32602  iundisjfi  32798  rdgssun  37379  evl1gprodd  42118  disjinfi  45197  fsumsermpt  45594  climsubmpt  45675  climeldmeqmpt  45683  climfveqmpt  45686  climfveqmpt3  45697  climeldmeqmpt3  45704  climinf2mpt  45729  climinfmpt  45730  dvmptmulf  45952  dvnmptdivc  45953  sge0lempt  46425  sge0isummpt2  46447  meadjiun  46481  hoimbl2  46680  vonhoire  46687
  Copyright terms: Public domain W3C validator