Theorem neli 3041

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

Syntax hints:  ¬ wn 3   ∈ wcel 2114   ∉ wnel 3039

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 210  df-nel 3040

This theorem is referenced by:  alephprc  9602  pnfnre2  10764  renepnf  10770  renemnf  10771  ltxrlt  10792  nn0nepnf  12059  xrltnr  12600  pnfnlt  12609  nltmnf  12610  hashclb  13814  hasheq0  13819  egt2lt3  15654  nthruc  15700  pcgcd1  16316  pc2dvds  16318  ramtcl2  16450  nsmndex1  18197  odhash3  18822  xrsmgmdifsgrp  20257  xrsdsreclblem  20266  topnex  21750  pnfnei  21974  mnfnei  21975  zclmncvs  23903  i1f0rn  24437  deg1nn0clb  24846  rgrx0ndm  27538  rgrx0nd  27539  f1resfz0f1d  32646  gonan0  32928  inaex  41480  mnfnre2  42497