![]() |
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.) |
Ref | Expression |
---|---|
nfs1v | ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbs1 2464 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | |
2 | 1 | nf5i 2064 | 1 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1748 [wsb 1937 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-10 2059 ax-12 2087 ax-13 2282 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-ex 1745 df-nf 1750 df-sb 1938 |
This theorem is referenced by: mo3 2536 eu1 2539 2mo 2580 2eu6 2587 cbvralf 3195 cbvralsv 3212 cbvrexsv 3213 cbvrab 3229 sbhypf 3284 mob2 3419 reu2 3427 reu2eqd 3436 sbcralt 3543 sbcreu 3548 cbvreucsf 3600 cbvrabcsf 3601 sbcel12 4016 sbceqg 4017 csbif 4171 cbvopab1 4756 cbvopab1s 4758 cbvmptf 4781 cbvmpt 4782 opelopabsb 5014 csbopab 5037 csbopabgALT 5038 opeliunxp 5204 ralxpf 5301 cbviota 5894 csbiota 5919 isarep1 6015 cbvriota 6661 csbriota 6663 onminex 7049 tfis 7096 findes 7138 abrexex2g 7186 abrexex2OLD 7192 dfoprab4f 7270 axrepndlem1 9452 axrepndlem2 9453 uzind4s 11786 mo5f 29452 ac6sf2 29557 esumcvg 30276 bj-mo3OLD 32957 wl-lem-moexsb 33480 wl-mo3t 33488 poimirlem26 33565 sbcalf 34047 sbcexf 34048 sbcrexgOLD 37666 sbcel12gOLD 39071 2sb5nd 39093 2sb5ndALT 39482 opeliun2xp 42436 |
Copyright terms: Public domain | W3C validator |