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

Theorem nfcsb1 3889
 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 3888 . 2 (⊤ → 𝑥𝐴 / 𝑥𝐵)
43mptru 1545 1 𝑥𝐴 / 𝑥𝐵
 Colors of variables: wff setvar class Syntax hints:  ⊤wtru 1539  Ⅎwnfc 2962  ⦋csb 3866 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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-sbc 3759  df-csb 3867 This theorem is referenced by:  nfcsb1v  3890  iundisj  24155  disjabrex  30343  disjabrexf  30344  iundisjf  30350  iundisjfi  30530  rdgssun  34740  disjinfi  41745  fsumsplit1  42140  fsumsermpt  42147  climsubmpt  42228  climeldmeqmpt  42236  climfveqmpt  42239  climfveqmpt3  42250  climeldmeqmpt3  42257  climinf2mpt  42282  climinfmpt  42283  dvmptmulf  42505  dvnmptdivc  42506  sge0f1o  42947  sge0lempt  42975  sge0isummpt2  42997  meadjiun  43031  hoimbl2  43230  vonhoire  43237
 Copyright terms: Public domain W3C validator