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

Theorem nfcsb1 3772
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 3771 . 2 (⊤ → 𝑥𝐴 / 𝑥𝐵)
43mptru 1664 1 𝑥𝐴 / 𝑥𝐵
Colors of variables: wff setvar class
Syntax hints:  wtru 1657  wnfc 2956  csb 3757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-sbc 3663  df-csb 3758
This theorem is referenced by:  nfcsb1v  3773  fprodsplit1f  15100  iundisj  23721  disjabrex  29938  disjabrexf  29939  iundisjf  29945  iundisjfi  30098  disjinfi  40183  fsumsplit1  40593  fsumsermpt  40600  climsubmpt  40681  climeldmeqmpt  40689  climfveqmpt  40692  climfveqmpt3  40703  climeldmeqmpt3  40710  climinf2mpt  40735  climinfmpt  40736  dvmptmulf  40941  dvnmptdivc  40942  sge0f1o  41384  sge0lempt  41412  sge0isummpt2  41434  meadjiun  41468  hoimbl2  41667  vonhoire  41674
  Copyright terms: Public domain W3C validator