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

Theorem nfcsb1 3581
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 3580 . 2 (⊤ → 𝑥𝐴 / 𝑥𝐵)
43trud 1533 1 𝑥𝐴 / 𝑥𝐵
Colors of variables: wff setvar class
Syntax hints:  wtru 1524  wnfc 2780  csb 3566
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  df-csb 3567
This theorem is referenced by:  nfcsb1v  3582  fprodsplit1f  14765  iundisj  23362  disjabrex  29521  disjabrexf  29522  iundisjf  29528  iundisjfi  29683  disjinfi  39694  fsumsplit1  40122  fsumsermpt  40129  climsubmpt  40210  climeldmeqmpt  40218  climfveqmpt  40221  climfveqmpt3  40232  climeldmeqmpt3  40239  climinf2mpt  40264  climinfmpt  40265  dvmptmulf  40470  dvnmptdivc  40471  sge0f1o  40917  sge0lempt  40945  sge0isummpt2  40967  meadjiun  41001  hoimbl2  41200  vonhoire  41207
  Copyright terms: Public domain W3C validator