| 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 3047. (Contributed by BJ, 7-Jul-2018.) |
| Ref | Expression |
|---|---|
| nelir.1 | ⊢ ¬ 𝐴 ∈ 𝐵 |
| Ref | Expression |
|---|---|
| nelir | ⊢ 𝐴 ∉ 𝐵 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nelir.1 | . 2 ⊢ ¬ 𝐴 ∈ 𝐵 | |
| 2 | df-nel 3047 | . 2 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) | |
| 3 | 1, 2 | mpbir 231 | 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: ru 3786 ruOLD 3787 prneli 4656 ruv 9642 ruALT 9643 cardprc 10020 pnfnre 11302 mnfnre 11304 eirr 16241 sqrt2irr 16285 lcmfnnval 16661 lcmf0 16671 smndex1n0mnd 18925 nsmndex1 18926 zringndrg 21479 topnex 23003 zfbas 23904 aaliou3 26393 finsumvtxdg2sstep 29567 xrge0iifcnv 33932 bj-0nel1 36954 bj-1nel0 36955 bj-0nelsngl 36972 ruvALT 42679 fmtnoinf 47523 fmtno5nprm 47570 4fppr1 47722 0nodd 48086 2nodd 48088 1neven 48154 2zrngnring 48174 |
| Copyright terms: Public domain | W3C validator |