![]() |
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 2157 and hbs1 2275 combined. (Revised by Wolf Lammen, 28-Jul-2022.) |
Ref | Expression |
---|---|
nfs1v | ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sb6 2085 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | |
2 | nfa1 2152 | . 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 = 𝑦 → 𝜑) | |
3 | 1, 2 | nfxfr 1851 | 1 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1535 Ⅎwnf 1781 [wsb 2064 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-10 2141 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-ex 1778 df-nf 1782 df-sb 2065 |
This theorem is referenced by: hbs1 2275 sb5OLD 2278 sb8fOLD 2360 sb8ef 2361 sbbib 2367 sb2ae 2504 mo3 2567 eu1 2613 2mo 2651 2eu6 2660 nfsab1 2725 cbvrexsvw 3324 cbvralsvwOLD 3325 cbvralsvwOLDOLD 3326 cbvrexsvwOLD 3327 cbvralf 3368 cbvralsv 3374 cbvrexsv 3375 cbvrabwOLD 3482 cbvrab 3487 sbhypfOLD 3557 mob2 3737 reu2 3747 reu2eqd 3758 sbcralt 3894 sbcreu 3898 cbvrabcsfw 3965 cbvreucsf 3968 cbvrabcsf 3969 sbcel12 4434 sbceqg 4435 2nreu 4467 csbif 4605 rexreusng 4703 cbvopab1 5241 cbvopab1g 5242 cbvopab1s 5244 cbvmptf 5275 cbvmptfg 5276 csbopab 5574 csbopabgALT 5575 opeliunxp 5767 ralxpf 5871 cbviotaw 6534 cbviota 6537 csbiota 6568 isarep1 6669 isarep1OLD 6670 f1ossf1o 7164 cbvriotaw 7415 cbvriota 7420 csbriota 7422 onminex 7840 tfis 7894 findes 7942 abrexex2g 8007 dfoprab4f 8099 axrepndlem1 10663 axrepndlem2 10664 uzind4s 12975 mo5f 32519 ac6sf2 32646 esumcvg 34052 bj-gabima 36908 wl-lem-moexsb 37524 wl-mo3t 37532 poimirlem26 37608 sbcalf 38076 sbcexf 38077 sbcrexgOLD 42743 scottabes 44213 2sb5nd 44533 2sb5ndALT 44905 2reu8i 47030 dfich2 47334 opeliun2xp 48059 |
Copyright terms: Public domain | W3C validator |