Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nfcsbw | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for substitution into a class. Version of nfcsb 3910 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by Mario Carneiro, 12-Oct-2016.) (Revised by Gino Giotto, 10-Jan-2024.) |
Ref | Expression |
---|---|
nfcsbw.1 | ⊢ Ⅎ𝑥𝐴 |
nfcsbw.2 | ⊢ Ⅎ𝑥𝐵 |
Ref | Expression |
---|---|
nfcsbw | ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-csb 3884 | . . 3 ⊢ ⦋𝐴 / 𝑦⦌𝐵 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝐵} | |
2 | nftru 1805 | . . . 4 ⊢ Ⅎ𝑧⊤ | |
3 | nftru 1805 | . . . . 5 ⊢ Ⅎ𝑦⊤ | |
4 | nfcsbw.1 | . . . . . 6 ⊢ Ⅎ𝑥𝐴 | |
5 | 4 | a1i 11 | . . . . 5 ⊢ (⊤ → Ⅎ𝑥𝐴) |
6 | nfcsbw.2 | . . . . . . 7 ⊢ Ⅎ𝑥𝐵 | |
7 | 6 | a1i 11 | . . . . . 6 ⊢ (⊤ → Ⅎ𝑥𝐵) |
8 | 7 | nfcrd 2969 | . . . . 5 ⊢ (⊤ → Ⅎ𝑥 𝑧 ∈ 𝐵) |
9 | 3, 5, 8 | nfsbcdw 3793 | . . . 4 ⊢ (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝑧 ∈ 𝐵) |
10 | 2, 9 | nfabdw 3000 | . . 3 ⊢ (⊤ → Ⅎ𝑥{𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝐵}) |
11 | 1, 10 | nfcxfrd 2976 | . 2 ⊢ (⊤ → Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵) |
12 | 11 | mptru 1544 | 1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ⊤wtru 1538 ∈ wcel 2114 {cab 2799 Ⅎwnfc 2961 [wsbc 3772 ⦋csb 3883 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-sbc 3773 df-csb 3884 |
This theorem is referenced by: cbvrabcsfw 3924 elfvmptrab1w 6794 fmptcof 6892 elovmporab1w 7392 mpomptsx 7762 dmmpossx 7764 fmpox 7765 el2mpocsbcl 7780 fmpoco 7790 dfmpo 7797 mpocurryd 7935 fvmpocurryd 7937 nfsumw 15047 fsum2dlem 15125 fsumcom2 15129 nfcprod 15265 fprod2dlem 15334 fprodcom2 15338 fsumcn 23478 fsum2cn 23479 dvmptfsum 24572 itgsubst 24646 iundisj2f 30340 f1od2 30457 esumiun 31353 poimirlem26 34933 cdlemkid 38087 cdlemk19x 38094 cdlemk11t 38097 wdom2d2 39681 dmmpossx2 44434 |
Copyright terms: Public domain | W3C validator |