![]() |
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 3922 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Mario Carneiro, 12-Oct-2016.) Avoid ax-13 2372. (Revised by Gino Giotto, 10-Jan-2024.) |
Ref | Expression |
---|---|
nfcsbw.1 | ⊢ Ⅎ𝑥𝐴 |
nfcsbw.2 | ⊢ Ⅎ𝑥𝐵 |
Ref | Expression |
---|---|
nfcsbw | ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-csb 3895 | . . 3 ⊢ ⦋𝐴 / 𝑦⦌𝐵 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝐵} | |
2 | nftru 1807 | . . . 4 ⊢ Ⅎ𝑧⊤ | |
3 | nftru 1807 | . . . . 5 ⊢ Ⅎ𝑦⊤ | |
4 | nfcsbw.1 | . . . . . 6 ⊢ Ⅎ𝑥𝐴 | |
5 | 4 | a1i 11 | . . . . 5 ⊢ (⊤ → Ⅎ𝑥𝐴) |
6 | nfcsbw.2 | . . . . . . 7 ⊢ Ⅎ𝑥𝐵 | |
7 | 6 | a1i 11 | . . . . . 6 ⊢ (⊤ → Ⅎ𝑥𝐵) |
8 | 7 | nfcrd 2893 | . . . . 5 ⊢ (⊤ → Ⅎ𝑥 𝑧 ∈ 𝐵) |
9 | 3, 5, 8 | nfsbcdw 3799 | . . . 4 ⊢ (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝑧 ∈ 𝐵) |
10 | 2, 9 | nfabdw 2927 | . . 3 ⊢ (⊤ → Ⅎ𝑥{𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝐵}) |
11 | 1, 10 | nfcxfrd 2903 | . 2 ⊢ (⊤ → Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵) |
12 | 11 | mptru 1549 | 1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ⊤wtru 1543 ∈ wcel 2107 {cab 2710 Ⅎwnfc 2884 [wsbc 3778 ⦋csb 3894 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-sbc 3779 df-csb 3895 |
This theorem is referenced by: cbvrabcsfw 3938 elfvmptrab1w 7025 fmptcof 7128 fvmpopr2d 7569 elovmporab1w 7653 mpomptsx 8050 dmmpossx 8052 fmpox 8053 el2mpocsbcl 8071 fmpoco 8081 dfmpo 8088 mpocurryd 8254 fvmpocurryd 8256 nfsum 15637 fsum2dlem 15716 fsumcom2 15720 nfcprod 15855 fprod2dlem 15924 fprodcom2 15928 fsumcn 24386 fsum2cn 24387 dvmptfsum 25492 itgsubst 25566 iundisj2f 31821 f1od2 31946 esumiun 33092 poimirlem26 36514 cdlemkid 39807 cdlemk19x 39814 cdlemk11t 39817 fmpocos 41056 wdom2d2 41774 dmmpossx2 47012 |
Copyright terms: Public domain | W3C validator |