Theorem neli 3038

Description: Inference associated with df-nel 3037. (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 3037	. 2 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)
3	1, 2	mpbi 230	1 ⊢ ¬ 𝐴 ∈ 𝐵

Syntax hints:  ¬ wn 3   ∈ wcel 2108   ∉ wnel 3036

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 3037

This theorem is referenced by:  alephprc  10113  pnfnre2  11277  renepnf  11283  renemnf  11284  ltxrlt  11305  nn0nepnf  12582  xrltnr  13135  pnfnlt  13144  nltmnf  13145  hashclb  14376  hasheq0  14381  egt2lt3  16224  nthruc  16270  pcgcd1  16897  pc2dvds  16899  ramtcl2  17031  nsmndex1  18891  odhash3  19557  xrsmgmdifsgrp  21371  xrsdsreclblem  21380  topnex  22934  pnfnei  23158  mnfnei  23159  zclmncvs  25100  i1f0rn  25635  deg1nn0clb  26047  rgrx0ndm  29573  rgrx0nd  29574  f1resfz0f1d  35136  gonan0  35414  inaex  44321  mnfnre2  45423  fonex  48842