![]() |
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 3855 with a disjoint variable condition, which does not require ax-13 2379. (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 3829 | . . 3 ⊢ ⦋𝐴 / 𝑦⦌𝐵 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝐵} | |
2 | nftru 1806 | . . . 4 ⊢ Ⅎ𝑧⊤ | |
3 | nftru 1806 | . . . . 5 ⊢ Ⅎ𝑦⊤ | |
4 | nfcsbw.1 | . . . . . 6 ⊢ Ⅎ𝑥𝐴 | |
5 | 4 | a1i 11 | . . . . 5 ⊢ (⊤ → Ⅎ𝑥𝐴) |
6 | nfcsbw.2 | . . . . . . 7 ⊢ Ⅎ𝑥𝐵 | |
7 | 6 | a1i 11 | . . . . . 6 ⊢ (⊤ → Ⅎ𝑥𝐵) |
8 | 7 | nfcrd 2945 | . . . . 5 ⊢ (⊤ → Ⅎ𝑥 𝑧 ∈ 𝐵) |
9 | 3, 5, 8 | nfsbcdw 3741 | . . . 4 ⊢ (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝑧 ∈ 𝐵) |
10 | 2, 9 | nfabdw 2976 | . . 3 ⊢ (⊤ → Ⅎ𝑥{𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝐵}) |
11 | 1, 10 | nfcxfrd 2954 | . 2 ⊢ (⊤ → Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵) |
12 | 11 | mptru 1545 | 1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ⊤wtru 1539 ∈ wcel 2111 {cab 2776 Ⅎwnfc 2936 [wsbc 3720 ⦋csb 3828 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-sbc 3721 df-csb 3829 |
This theorem is referenced by: cbvrabcsfw 3869 elfvmptrab1w 6771 fmptcof 6869 fvmpopr2d 7290 elovmporab1w 7372 mpomptsx 7744 dmmpossx 7746 fmpox 7747 el2mpocsbcl 7763 fmpoco 7773 dfmpo 7780 mpocurryd 7918 fvmpocurryd 7920 nfsum 15039 fsum2dlem 15117 fsumcom2 15121 nfcprod 15257 fprod2dlem 15326 fprodcom2 15330 fsumcn 23475 fsum2cn 23476 dvmptfsum 24578 itgsubst 24652 iundisj2f 30353 f1od2 30483 esumiun 31463 poimirlem26 35083 cdlemkid 38232 cdlemk19x 38239 cdlemk11t 38242 wdom2d2 39976 dmmpossx2 44738 |
Copyright terms: Public domain | W3C validator |