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 2783. (Contributed by BJ, 7-Jul-2018.) |
Ref | Expression |
---|---|
neli.1 | ⊢ 𝐴 ∉ 𝐵 |
Ref | Expression |
---|---|
neli | ⊢ ¬ 𝐴 ∈ 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neli.1 | . 2 ⊢ 𝐴 ∉ 𝐵 | |
2 | df-nel 2783 | . 2 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) | |
3 | 1, 2 | mpbi 219 | 1 ⊢ ¬ 𝐴 ∈ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∈ wcel 1977 ∉ wnel 2781 |
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 196 df-nel 2783 |
This theorem is referenced by: alephprc 8805 renepnf 9966 renemnf 9967 ltxrlt 9987 nn0nepnf 11248 xrltnr 11829 pnfnlt 11838 nltmnf 11839 hashclb 13011 hasheq0 13015 egt2lt3 14773 nthruc 14819 pcgcd1 15419 pc2dvds 15421 ramtcl2 15553 odhash3 17814 xrsmgmdifsgrp 19602 xrsdsreclblem 19611 pnfnei 20834 mnfnei 20835 zclmncvs 22756 i1f0rn 23255 deg1nn0clb 23654 bj-topnex 32247 rgrx0ndm 40793 rgrx0nd 40794 |
Copyright terms: Public domain | W3C validator |