![]() |
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 3878 | . 2 ⊢ (⊤ → Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵) |
4 | 3 | mptru 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 |