![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfex | GIF 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 1530 | . . 3 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | 2 | hbex 1647 | . 2 ⊢ (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑) |
4 | 3 | nfi 1473 | 1 ⊢ Ⅎ𝑥∃𝑦𝜑 |
Colors of variables: wff set class |
Syntax hints: Ⅎwnf 1471 ∃wex 1503 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-4 1521 |
This theorem depends on definitions: df-bi 117 df-nf 1472 |
This theorem is referenced by: eeor 1706 cbvexv1 1763 cbvex2 1934 eean 1943 nfsbv 1959 nfeu1 2049 nfeuv 2056 nfel 2341 ceqsex2 2792 nfopab 4086 nfopab2 4088 cbvopab1 4091 cbvopab1s 4093 repizf2 4180 copsex2t 4263 copsex2g 4264 euotd 4272 onintrab2im 4535 mosubopt 4709 nfco 4810 dfdmf 4838 dfrnf 4886 nfdm 4889 fv3 5557 nfoprab2 5947 nfoprab3 5948 nfoprab 5949 cbvoprab1 5969 cbvoprab2 5970 cbvoprab3 5973 cnvoprab 6260 ac6sfi 6927 cc3 7298 nfsum1 11399 nfsum 11400 fsum2dlemstep 11477 nfcprod1 11597 nfcprod 11598 fprod2dlemstep 11665 lss1d 13716 |
Copyright terms: Public domain | W3C validator |