![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfcsb | 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 |
---|---|
nfcsb.1 | ⊢ Ⅎ𝑥𝐴 |
nfcsb.2 | ⊢ Ⅎ𝑥𝐵 |
Ref | Expression |
---|---|
nfcsb | ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nftru 1770 | . . 3 ⊢ Ⅎ𝑦⊤ | |
2 | nfcsb.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝐴) |
4 | nfcsb.2 | . . . 4 ⊢ Ⅎ𝑥𝐵 | |
5 | 4 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝐵) |
6 | 1, 3, 5 | nfcsbd 3583 | . 2 ⊢ (⊤ → Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵) |
7 | 6 | trud 1533 | 1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ⊤wtru 1524 Ⅎwnfc 2780 ⦋csb 3566 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-sbc 3469 df-csb 3567 |
This theorem is referenced by: cbvralcsf 3598 cbvreucsf 3600 cbvrabcsf 3601 elfvmptrab1 6344 fmptcof 6437 elovmpt2rab1 6923 mpt2mptsx 7278 dmmpt2ssx 7280 fmpt2x 7281 el2mpt2csbcl 7295 fmpt2co 7305 dfmpt2 7312 mpt2curryd 7440 fvmpt2curryd 7442 nfsum 14465 fsum2dlem 14545 fsumcom2 14549 fsumcom2OLD 14550 nfcprod 14685 fprod2dlem 14754 fprodcom2 14758 fprodcom2OLD 14759 fsumcn 22720 fsum2cn 22721 dvmptfsum 23783 itgsubst 23857 iundisj2f 29529 f1od2 29627 esumiun 30284 poimirlem26 33565 cdlemkid 36541 cdlemk19x 36548 cdlemk11t 36551 wdom2d2 37919 dmmpt2ssx2 42440 |
Copyright terms: Public domain | W3C validator |