Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfs1v | Unicode version |
Description: is not free in when and are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfs1v |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbs1 1918 | . 2 | |
2 | 1 | nfi 1442 | 1 |
Colors of variables: wff set class |
Syntax hints: wnf 1440 wsb 1742 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1427 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-11 1486 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 |
This theorem depends on definitions: df-bi 116 df-nf 1441 df-sb 1743 |
This theorem is referenced by: nfsbxy 1922 nfsbxyt 1923 sbco3v 1949 sbcomxyyz 1952 sbnf2 1961 mo2n 2034 mo23 2047 mor 2048 clelab 2283 cbvralf 2674 cbvrexf 2675 cbvralsv 2694 cbvrexsv 2695 cbvrab 2710 sbhypf 2761 mob2 2892 reu2 2900 sbcralt 3013 sbcrext 3014 sbcralg 3015 sbcreug 3017 sbcel12g 3046 sbceqg 3047 cbvreucsf 3095 cbvrabcsf 3096 disjiun 3962 cbvopab1 4039 cbvopab1s 4041 csbopabg 4044 cbvmptf 4060 cbvmpt 4061 opelopabsb 4222 frind 4314 tfis 4544 findes 4564 opeliunxp 4643 ralxpf 4734 rexxpf 4735 cbviota 5142 csbiotag 5165 isarep1 5258 cbvriota 5792 csbriotag 5794 abrexex2g 6070 abrexex2 6074 dfoprab4f 6143 finexdc 6849 ssfirab 6880 uzind4s 9506 zsupcllemstep 11844 bezoutlemmain 11897 cbvrald 13433 bj-bdfindes 13595 bj-findes 13627 |
Copyright terms: Public domain | W3C validator |