![]() |
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 3771 | . 2 ⊢ (⊤ → Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵) |
4 | 3 | mptru 1664 | 1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ⊤wtru 1657 Ⅎwnfc 2956 ⦋csb 3757 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-sbc 3663 df-csb 3758 |
This theorem is referenced by: nfcsb1v 3773 fprodsplit1f 15100 iundisj 23721 disjabrex 29938 disjabrexf 29939 iundisjf 29945 iundisjfi 30098 disjinfi 40183 fsumsplit1 40593 fsumsermpt 40600 climsubmpt 40681 climeldmeqmpt 40689 climfveqmpt 40692 climfveqmpt3 40703 climeldmeqmpt3 40710 climinf2mpt 40735 climinfmpt 40736 dvmptmulf 40941 dvnmptdivc 40942 sge0f1o 41384 sge0lempt 41412 sge0isummpt2 41434 meadjiun 41468 hoimbl2 41667 vonhoire 41674 |
Copyright terms: Public domain | W3C validator |