Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfsb | Unicode version |
Description: If is not free in , it is not free in when and are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof rewritten by Jim Kingdon, 19-Mar-2018.) |
Ref | Expression |
---|---|
nfsb.1 |
Ref | Expression |
---|---|
nfsb |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfsb.1 | . . . 4 | |
2 | 1 | nfsbxy 1895 | . . 3 |
3 | 2 | nfsbxy 1895 | . 2 |
4 | ax-17 1491 | . . . 4 | |
5 | 4 | sbco2v 1898 | . . 3 |
6 | 5 | nfbii 1434 | . 2 |
7 | 3, 6 | mpbi 144 | 1 |
Colors of variables: wff set class |
Syntax hints: wnf 1421 wsb 1720 |
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-io 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-sb 1721 |
This theorem is referenced by: hbsb 1900 sbco2yz 1914 sbcomxyyz 1923 hbsbd 1935 nfsb4or 1976 sb8eu 1990 nfeu 1996 cbvab 2240 cbvralf 2625 cbvrexf 2626 cbvreu 2629 cbvralsv 2642 cbvrexsv 2643 cbvrab 2658 cbvreucsf 3034 cbvrabcsf 3035 cbvopab1 3971 cbvmptf 3992 cbvmpt 3993 ralxpf 4655 rexxpf 4656 cbviota 5063 sb8iota 5065 cbvriota 5708 dfoprab4f 6059 |
Copyright terms: Public domain | W3C validator |