![]() |
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 3931 | . 2 ⊢ (⊤ → Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵) |
4 | 3 | mptru 1544 | 1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ⊤wtru 1538 Ⅎwnfc 2888 ⦋csb 3908 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1540 df-ex 1777 df-nf 1781 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-sbc 3792 df-csb 3909 |
This theorem is referenced by: nfcsb1v 3933 fsumsplit1 15778 iundisj 25597 disjabrex 32602 disjabrexf 32603 iundisjf 32609 iundisjfi 32804 rdgssun 37361 evl1gprodd 42099 disjinfi 45135 fsumsermpt 45535 climsubmpt 45616 climeldmeqmpt 45624 climfveqmpt 45627 climfveqmpt3 45638 climeldmeqmpt3 45645 climinf2mpt 45670 climinfmpt 45671 dvmptmulf 45893 dvnmptdivc 45894 sge0lempt 46366 sge0isummpt2 46388 meadjiun 46422 hoimbl2 46621 vonhoire 46628 |
Copyright terms: Public domain | W3C validator |