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 3124. (Contributed by BJ, 7-Jul-2018.) |
Ref | Expression |
---|---|
neli.1 | ⊢ 𝐴 ∉ 𝐵 |
Ref | Expression |
---|---|
neli | ⊢ ¬ 𝐴 ∈ 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neli.1 | . 2 ⊢ 𝐴 ∉ 𝐵 | |
2 | df-nel 3124 | . 2 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) | |
3 | 1, 2 | mpbi 231 | 1 ⊢ ¬ 𝐴 ∈ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∈ wcel 2105 ∉ wnel 3123 |
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 208 df-nel 3124 |
This theorem is referenced by: alephprc 9514 pnfnre2 10672 renepnf 10678 renemnf 10679 ltxrlt 10700 nn0nepnf 11964 xrltnr 12504 pnfnlt 12513 nltmnf 12514 hashclb 13709 hasheq0 13714 egt2lt3 15549 nthruc 15595 pcgcd1 16203 pc2dvds 16205 ramtcl2 16337 odhash3 18632 xrsmgmdifsgrp 20512 xrsdsreclblem 20521 topnex 21534 pnfnei 21758 mnfnei 21759 zclmncvs 23681 i1f0rn 24212 deg1nn0clb 24613 rgrx0ndm 27303 rgrx0nd 27304 f1resfz0f1d 32259 gonan0 32537 inaex 40513 mnfnre2 41548 nsmndex1 43983 |
Copyright terms: Public domain | W3C validator |