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

Theorem nfcsb1 3879
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 3878 . 2 (⊤ → 𝑥𝐴 / 𝑥𝐵)
43mptru 1548 1 𝑥𝐴 / 𝑥𝐵
Colors of variables: wff setvar class
Syntax hints:  wtru 1542  wnfc 2887  csb 3855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-sbc 3740  df-csb 3856
This theorem is referenced by:  nfcsb1v  3880  fsumsplit1  15629  iundisj  24910  disjabrex  31447  disjabrexf  31448  iundisjf  31454  iundisjfi  31643  rdgssun  35839  disjinfi  43387  fsumsermpt  43791  climsubmpt  43872  climeldmeqmpt  43880  climfveqmpt  43883  climfveqmpt3  43894  climeldmeqmpt3  43901  climinf2mpt  43926  climinfmpt  43927  dvmptmulf  44149  dvnmptdivc  44150  sge0f1o  44594  sge0lempt  44622  sge0isummpt2  44644  meadjiun  44678  hoimbl2  44877  vonhoire  44884
  Copyright terms: Public domain W3C validator