![]() |
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 3037. (Contributed by BJ, 7-Jul-2018.) |
Ref | Expression |
---|---|
neli.1 | ⊢ 𝐴 ∉ 𝐵 |
Ref | Expression |
---|---|
neli | ⊢ ¬ 𝐴 ∈ 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neli.1 | . 2 ⊢ 𝐴 ∉ 𝐵 | |
2 | df-nel 3037 | . 2 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) | |
3 | 1, 2 | mpbi 220 | 1 ⊢ ¬ 𝐴 ∈ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∈ wcel 2140 ∉ wnel 3036 |
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 197 df-nel 3037 |
This theorem is referenced by: alephprc 9133 renepnf 10300 renemnf 10301 ltxrlt 10321 nn0nepnf 11584 xrltnr 12167 pnfnlt 12176 nltmnf 12177 hashclb 13362 hasheq0 13367 egt2lt3 15154 nthruc 15201 pcgcd1 15804 pc2dvds 15806 ramtcl2 15938 odhash3 18212 xrsmgmdifsgrp 20006 xrsdsreclblem 20015 topnex 21023 pnfnei 21247 mnfnei 21248 zclmncvs 23169 i1f0rn 23669 deg1nn0clb 24070 rgrx0ndm 26721 rgrx0nd 26722 mnfnre2 40136 pnfnre2 40145 |
Copyright terms: Public domain | W3C validator |