![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfre1 | GIF version |
Description: 𝑥 is not free in ∃𝑥 ∈ 𝐴𝜑. (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Ref | Expression |
---|---|
nfre1 | ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rex 2361 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | nfe1 1428 | . 2 ⊢ Ⅎ𝑥∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) | |
3 | 1, 2 | nfxfr 1406 | 1 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑 |
Colors of variables: wff set class |
Syntax hints: ∧ wa 102 Ⅎwnf 1392 ∃wex 1424 ∈ wcel 1436 ∃wrex 2356 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1379 ax-gen 1381 ax-ie1 1425 |
This theorem depends on definitions: df-bi 115 df-nf 1393 df-rex 2361 |
This theorem is referenced by: nfiu1 3737 fun11iun 5225 eusvobj2 5580 fodjuomnilemdc 6720 prarloclem3step 6976 prmuloc2 7047 ltexprlemm 7080 caucvgprprlemaddq 7188 caucvgsrlemgt1 7261 supinfneg 8992 infsupneg 8993 lbzbi 9010 divalglemeunn 10715 divalglemeuneg 10717 bezoutlemmain 10781 bezout 10794 |
Copyright terms: Public domain | W3C validator |