![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfs1v | Structured version Visualization version GIF version |
Description: The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) Shorten nfs1v and hbs1 2314 combined. (Revised by Wolf Lammen, 28-Jul-2022.) |
Ref | Expression |
---|---|
nfs1v | ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sb6 2309 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | |
2 | nfa1 2204 | . 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 = 𝑦 → 𝜑) | |
3 | 1, 2 | nfxfr 1954 | 1 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1656 Ⅎwnf 1884 [wsb 2069 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-10 2194 ax-12 2222 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-ex 1881 df-nf 1885 df-sb 2070 |
This theorem is referenced by: hbs1 2314 sb8v 2378 sb8ev 2379 mo3 2633 mo3OLD 2634 eu1 2695 eu1OLD 2696 2mo 2731 2eu6 2738 cbvralf 3377 cbvralsv 3394 cbvrexsv 3395 cbvrab 3411 sbhypf 3470 mob2 3611 reu2 3619 reu2eqd 3630 sbcralt 3735 sbcreu 3739 cbvreucsf 3791 cbvrabcsf 3792 sbcel12 4207 sbceqg 4208 csbif 4361 cbvopab1 4946 cbvopab1s 4948 cbvmptf 4971 cbvmpt 4972 opelopabsb 5211 csbopab 5234 csbopabgALT 5235 opeliunxp 5403 ralxpf 5501 cbviota 6091 csbiota 6116 isarep1 6210 f1ossf1o 6645 cbvriota 6876 csbriota 6878 onminex 7268 tfis 7315 findes 7357 abrexex2g 7405 dfoprab4f 7488 axrepndlem1 9729 axrepndlem2 9730 uzind4s 12030 mo5f 29879 ac6sf2 29978 esumcvg 30693 bj-mo3OLD 33356 wl-lem-moexsb 33894 wl-mo3t 33902 poimirlem26 33979 sbcalf 34458 sbcexf 34459 sbcrexgOLD 38193 2sb5nd 39604 2sb5ndALT 39986 opeliun2xp 42958 |
Copyright terms: Public domain | W3C validator |