Theorem neli 3125

Description: Inference associated with df-nel 3124. (Contributed by BJ, 7-Jul-2018.)

Hypothesis

Ref	Expression
neli.1	⊢ 𝐴 ∉ 𝐵

Assertion

Ref	Expression
neli	⊢ ¬ 𝐴 ∈ 𝐵

Proof of Theorem neli

Step	Hyp	Ref	Expression
1		neli.1	. 2 ⊢ 𝐴 ∉ 𝐵
2		df-nel 3124	. 2 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)
3	1, 2	mpbi 232	1 ⊢ ¬ 𝐴 ∈ 𝐵

Syntax hints:  ¬ wn 3   ∈ wcel 2114   ∉ 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 209  df-nel 3124

This theorem is referenced by:  alephprc  9525  pnfnre2  10683  renepnf  10689  renemnf  10690  ltxrlt  10711  nn0nepnf  11976  xrltnr  12515  pnfnlt  12524  nltmnf  12525  hashclb  13720  hasheq0  13725  egt2lt3  15559  nthruc  15605  pcgcd1  16213  pc2dvds  16215  ramtcl2  16347  nsmndex1  18078  odhash3  18701  xrsmgmdifsgrp  20582  xrsdsreclblem  20591  topnex  21604  pnfnei  21828  mnfnei  21829  zclmncvs  23752  i1f0rn  24283  deg1nn0clb  24684  rgrx0ndm  27375  rgrx0nd  27376  f1resfz0f1d  32361  gonan0  32639  inaex  40653  mnfnre2  41688