| 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 3047. (Contributed by BJ, 7-Jul-2018.) |
| Ref | Expression |
|---|---|
| neli.1 | ⊢ 𝐴 ∉ 𝐵 |
| Ref | Expression |
|---|---|
| neli | ⊢ ¬ 𝐴 ∈ 𝐵 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | neli.1 | . 2 ⊢ 𝐴 ∉ 𝐵 | |
| 2 | df-nel 3047 | . 2 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) | |
| 3 | 1, 2 | mpbi 230 | 1 ⊢ ¬ 𝐴 ∈ 𝐵 |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ∈ wcel 2108 ∉ wnel 3046 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 df-nel 3047 |
| This theorem is referenced by: alephprc 10139 pnfnre2 11303 renepnf 11309 renemnf 11310 ltxrlt 11331 nn0nepnf 12607 xrltnr 13161 pnfnlt 13170 nltmnf 13171 hashclb 14397 hasheq0 14402 egt2lt3 16242 nthruc 16288 pcgcd1 16915 pc2dvds 16917 ramtcl2 17049 nsmndex1 18926 odhash3 19594 xrsmgmdifsgrp 21421 xrsdsreclblem 21430 topnex 23003 pnfnei 23228 mnfnei 23229 zclmncvs 25182 i1f0rn 25717 deg1nn0clb 26129 rgrx0ndm 29611 rgrx0nd 29612 f1resfz0f1d 35119 gonan0 35397 inaex 44316 mnfnre2 45407 |
| Copyright terms: Public domain | W3C validator |