Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfex | Unicode version |
Description: If is not free in , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) |
Ref | Expression |
---|---|
nfex.1 |
Ref | Expression |
---|---|
nfex |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfex.1 | . . . 4 | |
2 | 1 | nfri 1499 | . . 3 |
3 | 2 | hbex 1615 | . 2 |
4 | 3 | nfi 1438 | 1 |
Colors of variables: wff set class |
Syntax hints: wnf 1436 wex 1468 |
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 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 |
This theorem depends on definitions: df-bi 116 df-nf 1437 |
This theorem is referenced by: eeor 1673 cbvex2 1894 eean 1903 nfeu1 2010 nfeuv 2017 nfel 2290 ceqsex2 2726 nfopab 3996 nfopab2 3998 cbvopab1 4001 cbvopab1s 4003 repizf2 4086 copsex2t 4167 copsex2g 4168 euotd 4176 onintrab2im 4434 mosubopt 4604 nfco 4704 dfdmf 4732 dfrnf 4780 nfdm 4783 fv3 5444 nfoprab2 5821 nfoprab3 5822 nfoprab 5823 cbvoprab1 5843 cbvoprab2 5844 cbvoprab3 5847 cnvoprab 6131 ac6sfi 6792 nfsum1 11125 nfsum 11126 fsum2dlemstep 11203 nfcprod1 11323 nfcprod 11324 |
Copyright terms: Public domain | W3C validator |