| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > neli | Structured version Visualization version GIF version | ||
| Description: Inference associated with df-nel 3067. (Contributed by BJ, 7-Jul-2018.) |
| Ref | Expression |
|---|---|
| neli.1 | ⊢ 𝐴 ∉ 𝐵 |
| Ref | Expression |
|---|---|
| neli | ⊢ ¬ 𝐴 ∈ 𝐵 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | neli.1 | . 2 ⊢ 𝐴 ∉ 𝐵 | |
| 2 | df-nel 3067 | . 2 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) | |
| 3 | 1, 2 | mpbi 233 | 1 ⊢ ¬ 𝐴 ∈ 𝐵 |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: ¬ wn 3 ∈ wcel 2146 ∉ wnel 3066 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This proof depends on definitions: df-bi 210 df-nel 3067 |
| This theorem is used by: alephprc 10099 pnfnre2 11270 renepnf 11276 renemnf 11277 ltxrlt 11299 nn0nepnf 12604 xrltnr 13164 pnfnlt 13173 nltmnf 13174 f1resfz0f1d 13842 hashclb 14416 hasheq0 14421 egt2lt3 16288 nthruc 16334 pcgcd1 16963 pc2dvds 16965 ramtcl2 17097 nsmndex1 19016 odhash3 19694 xrsmgmdifsgrp 21613 xrsdsreclblem 21617 topnex 23207 pnfnei 23431 mnfnei 23432 zclmncvs 25362 i1f0rn 25896 deg1nn0clb 26302 rgrx0ndm 30005 rgrx0nd 30006 nowisdomv 30900 ply1coedeg 33947 trisecnconstr 34250 gonan0 35925 inaex 45084 mnfnre2 46188 nthrucw 47684 fonex 49721 |
| Copyright terms: Public domain | W3C validator |