| 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 3921 | . 2 ⊢ (⊤ → Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵) |
| 4 | 3 | mptru 1547 | 1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 |
| Colors of variables: wff setvar class |
| Syntax hints: ⊤wtru 1541 Ⅎwnfc 2890 ⦋csb 3899 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-sbc 3789 df-csb 3900 |
| This theorem is referenced by: nfcsb1v 3923 fsumsplit1 15781 iundisj 25583 disjabrex 32595 disjabrexf 32596 iundisjf 32602 iundisjfi 32798 rdgssun 37379 evl1gprodd 42118 disjinfi 45197 fsumsermpt 45594 climsubmpt 45675 climeldmeqmpt 45683 climfveqmpt 45686 climfveqmpt3 45697 climeldmeqmpt3 45704 climinf2mpt 45729 climinfmpt 45730 dvmptmulf 45952 dvnmptdivc 45953 sge0lempt 46425 sge0isummpt2 46447 meadjiun 46481 hoimbl2 46680 vonhoire 46687 |
| Copyright terms: Public domain | W3C validator |