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 1412 | . . 3 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | 2 | hbex 1527 | . 2 ⊢ (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑) |
4 | 3 | nfi 1351 | 1 ⊢ Ⅎ𝑥∃𝑦𝜑 |
Colors of variables: wff set class |
Syntax hints: Ⅎwnf 1349 ∃wex 1381 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 |
This theorem depends on definitions: df-bi 110 df-nf 1350 |
This theorem is referenced by: eeor 1585 cbvex2 1797 eean 1806 nfeu1 1911 nfeuv 1918 nfel 2186 ceqsex2 2594 nfopab 3825 nfopab2 3827 cbvopab1 3830 cbvopab1s 3832 repizf2 3915 copsex2t 3982 copsex2g 3983 euotd 3991 onintrab2im 4244 mosubopt 4405 nfco 4501 dfdmf 4528 dfrnf 4575 nfdm 4578 fv3 5197 nfoprab2 5555 nfoprab3 5556 nfoprab 5557 cbvoprab1 5576 cbvoprab2 5577 cbvoprab3 5580 ac6sfi 6352 nfsum1 9875 nfsum 9876 |
Copyright terms: Public domain | W3C validator |