Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nelir | Structured version Visualization version GIF version |
Description: Inference associated with df-nel 3124. (Contributed by BJ, 7-Jul-2018.) |
Ref | Expression |
---|---|
nelir.1 | ⊢ ¬ 𝐴 ∈ 𝐵 |
Ref | Expression |
---|---|
nelir | ⊢ 𝐴 ∉ 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nelir.1 | . 2 ⊢ ¬ 𝐴 ∈ 𝐵 | |
2 | df-nel 3124 | . 2 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) | |
3 | 1, 2 | mpbir 232 | 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: ru 3770 prneli 4587 ruv 9055 ruALT 9056 cardprc 9398 pnfnre 10671 mnfnre 10673 wrdlndmOLD 13870 eirr 15548 sqrt2irr 15592 lcmfnnval 15958 lcmf0 15968 zringndrg 20567 topnex 21534 zfbas 22434 aaliou3 24869 finsumvtxdg2sstep 27259 xrge0iifcnv 31076 bj-0nel1 34163 bj-1nel0 34164 bj-0nelsngl 34181 fmtnoinf 43545 fmtno5nprm 43592 4fppr1 43747 0nodd 43924 2nodd 43926 smndex1n0mnd 43982 nsmndex1 43983 1neven 44101 2zrngnring 44121 |
Copyright terms: Public domain | W3C validator |