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 3513 | . 2 ⊢ (⊤ → Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵) |
4 | 3 | trud 1484 | 1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ⊤wtru 1476 Ⅎwnfc 2738 ⦋csb 3499 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-sbc 3403 df-csb 3500 |
This theorem is referenced by: nfcsb1v 3515 fprodsplit1f 14560 iundisj 23123 disjabrex 28777 disjabrexf 28778 iundisjf 28784 iundisjfi 28942 disjinfi 38375 fsumsplit1 38639 fsumsermpt 38646 climsubmpt 38727 climeldmeqmpt 38735 climfveqmpt 38738 dvmptmulf 38827 dvnmptdivc 38828 sge0f1o 39275 sge0lempt 39303 sge0isummpt2 39325 meadjiun 39359 hoimbl2 39555 vonhoire 39563 |
Copyright terms: Public domain | W3C validator |