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 1512 | . . 3 |
3 | 2 | hbex 1629 | . 2 |
4 | 3 | nfi 1455 | 1 |
Colors of variables: wff set class |
Syntax hints: wnf 1453 wex 1485 |
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 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-4 1503 |
This theorem depends on definitions: df-bi 116 df-nf 1454 |
This theorem is referenced by: eeor 1688 cbvexv1 1745 cbvex2 1915 eean 1924 nfsbv 1940 nfeu1 2030 nfeuv 2037 nfel 2321 ceqsex2 2770 nfopab 4057 nfopab2 4059 cbvopab1 4062 cbvopab1s 4064 repizf2 4148 copsex2t 4230 copsex2g 4231 euotd 4239 onintrab2im 4502 mosubopt 4676 nfco 4776 dfdmf 4804 dfrnf 4852 nfdm 4855 fv3 5519 nfoprab2 5903 nfoprab3 5904 nfoprab 5905 cbvoprab1 5925 cbvoprab2 5926 cbvoprab3 5929 cnvoprab 6213 ac6sfi 6876 cc3 7230 nfsum1 11319 nfsum 11320 fsum2dlemstep 11397 nfcprod1 11517 nfcprod 11518 fprod2dlemstep 11585 |
Copyright terms: Public domain | W3C validator |