Theorem neli 3093

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

Syntax hints:  ¬ wn 3   ∈ wcel 2111   ∉ wnel 3091

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 3092

This theorem is referenced by:  alephprc  9510  pnfnre2  10672  renepnf  10678  renemnf  10679  ltxrlt  10700  nn0nepnf  11963  xrltnr  12502  pnfnlt  12511  nltmnf  12512  hashclb  13715  hasheq0  13720  egt2lt3  15551  nthruc  15597  pcgcd1  16203  pc2dvds  16205  ramtcl2  16337  nsmndex1  18070  odhash3  18693  xrsmgmdifsgrp  20128  xrsdsreclblem  20137  topnex  21601  pnfnei  21825  mnfnei  21826  zclmncvs  23753  i1f0rn  24286  deg1nn0clb  24691  rgrx0ndm  27383  rgrx0nd  27384  f1resfz0f1d  32471  gonan0  32752  inaex  41005  mnfnre2  42032