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 1616 | . 2 |
4 | 3 | nfi 1442 | 1 |
Colors of variables: wff set class |
Syntax hints: wnf 1440 wex 1472 |
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-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-4 1490 |
This theorem depends on definitions: df-bi 116 df-nf 1441 |
This theorem is referenced by: eeor 1675 cbvexv1 1732 cbvex2 1902 eean 1911 nfsbv 1927 nfeu1 2017 nfeuv 2024 nfel 2308 ceqsex2 2752 nfopab 4034 nfopab2 4036 cbvopab1 4039 cbvopab1s 4041 repizf2 4125 copsex2t 4207 copsex2g 4208 euotd 4216 onintrab2im 4479 mosubopt 4653 nfco 4753 dfdmf 4781 dfrnf 4829 nfdm 4832 fv3 5493 nfoprab2 5873 nfoprab3 5874 nfoprab 5875 cbvoprab1 5895 cbvoprab2 5896 cbvoprab3 5899 cnvoprab 6183 ac6sfi 6845 cc3 7190 nfsum1 11264 nfsum 11265 fsum2dlemstep 11342 nfcprod1 11462 nfcprod 11463 fprod2dlemstep 11530 |
Copyright terms: Public domain | W3C validator |