![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfcsb1 | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.) |
Ref | Expression |
---|---|
nfcsb1.1 | ⊢ Ⅎ𝑥𝐴 |
Ref | Expression |
---|---|
nfcsb1 | ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcsb1.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
2 | 1 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝐴) |
3 | 2 | nfcsb1d 3915 | . 2 ⊢ (⊤ → Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵) |
4 | 3 | mptru 1541 | 1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ⊤wtru 1535 Ⅎwnfc 2876 ⦋csb 3892 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1537 df-ex 1775 df-nf 1779 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-sbc 3777 df-csb 3893 |
This theorem is referenced by: nfcsb1v 3917 fsumsplit1 15742 iundisj 25563 disjabrex 32500 disjabrexf 32501 iundisjf 32507 iundisjfi 32699 rdgssun 37096 evl1gprodd 41827 disjinfi 44833 fsumsermpt 45234 climsubmpt 45315 climeldmeqmpt 45323 climfveqmpt 45326 climfveqmpt3 45337 climeldmeqmpt3 45344 climinf2mpt 45369 climinfmpt 45370 dvmptmulf 45592 dvnmptdivc 45593 sge0f1o 46037 sge0lempt 46065 sge0isummpt2 46087 meadjiun 46121 hoimbl2 46320 vonhoire 46327 |
Copyright terms: Public domain | W3C validator |