![]() |
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 2154 and hbs1 2266 combined. (Revised by Wolf Lammen, 28-Jul-2022.) |
Ref | Expression |
---|---|
nfs1v | ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sb6 2089 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | |
2 | nfa1 2149 | . 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 = 𝑦 → 𝜑) | |
3 | 1, 2 | nfxfr 1856 | 1 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 Ⅎwnf 1786 [wsb 2068 |
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-10 2138 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-ex 1783 df-nf 1787 df-sb 2069 |
This theorem is referenced by: hbs1 2266 sb5OLD 2269 sb8fOLD 2351 sb8ef 2352 sbbib 2358 sb2ae 2496 mo3 2559 eu1 2607 2mo 2645 2eu6 2653 nfsab1 2718 cbvralsvw 3315 cbvrexsvw 3316 cbvralsvwOLD 3317 cbvrexsvwOLD 3318 cbvralfwOLD 3321 cbvralf 3357 cbvralsv 3363 cbvrexsv 3364 cbvrabw 3468 cbvrab 3474 sbhypfOLD 3539 mob2 3710 reu2 3720 reu2eqd 3731 sbcralt 3865 sbcreu 3869 cbvrabcsfw 3936 cbvreucsf 3939 cbvrabcsf 3940 sbcel12 4407 sbceqg 4408 2nreu 4440 csbif 4584 rexreusng 4682 cbvopab1 5222 cbvopab1g 5223 cbvopab1s 5225 cbvmptf 5256 cbvmptfg 5257 csbopab 5554 csbopabgALT 5555 opeliunxp 5741 ralxpf 5844 cbviotaw 6499 cbviota 6502 csbiota 6533 isarep1 6634 isarep1OLD 6635 f1ossf1o 7121 cbvriotaw 7369 cbvriota 7374 csbriota 7376 onminex 7785 tfis 7839 findes 7888 abrexex2g 7946 dfoprab4f 8037 axrepndlem1 10583 axrepndlem2 10584 uzind4s 12888 mo5f 31707 ac6sf2 31827 esumcvg 33022 bj-gabima 35758 wl-lem-moexsb 36371 wl-mo3t 36379 poimirlem26 36452 sbcalf 36920 sbcexf 36921 sbcrexgOLD 41456 scottabes 42934 2sb5nd 43254 2sb5ndALT 43626 2reu8i 45756 dfich2 46061 opeliun2xp 46910 |
Copyright terms: Public domain | W3C validator |