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 1517 | . . 3 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | 2 | hbex 1634 | . 2 ⊢ (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑) |
4 | 3 | nfi 1460 | 1 ⊢ Ⅎ𝑥∃𝑦𝜑 |
Colors of variables: wff set class |
Syntax hints: Ⅎwnf 1458 ∃wex 1490 |
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 1445 ax-7 1446 ax-gen 1447 ax-ie1 1491 ax-ie2 1492 ax-4 1508 |
This theorem depends on definitions: df-bi 117 df-nf 1459 |
This theorem is referenced by: eeor 1693 cbvexv1 1750 cbvex2 1920 eean 1929 nfsbv 1945 nfeu1 2035 nfeuv 2042 nfel 2326 ceqsex2 2775 nfopab 4066 nfopab2 4068 cbvopab1 4071 cbvopab1s 4073 repizf2 4157 copsex2t 4239 copsex2g 4240 euotd 4248 onintrab2im 4511 mosubopt 4685 nfco 4785 dfdmf 4813 dfrnf 4861 nfdm 4864 fv3 5530 nfoprab2 5915 nfoprab3 5916 nfoprab 5917 cbvoprab1 5937 cbvoprab2 5938 cbvoprab3 5941 cnvoprab 6225 ac6sfi 6888 cc3 7242 nfsum1 11331 nfsum 11332 fsum2dlemstep 11409 nfcprod1 11529 nfcprod 11530 fprod2dlemstep 11597 |
Copyright terms: Public domain | W3C validator |