Theorem neli 3031

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

Syntax hints:  ¬ wn 3   ∈ wcel 2109   ∉ wnel 3029

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 3030

This theorem is referenced by:  alephprc  10052  pnfnre2  11216  renepnf  11222  renemnf  11223  ltxrlt  11244  nn0nepnf  12523  xrltnr  13079  pnfnlt  13088  nltmnf  13089  hashclb  14323  hasheq0  14328  egt2lt3  16174  nthruc  16220  pcgcd1  16848  pc2dvds  16850  ramtcl2  16982  nsmndex1  18840  odhash3  19506  xrsmgmdifsgrp  21320  xrsdsreclblem  21329  topnex  22883  pnfnei  23107  mnfnei  23108  zclmncvs  25048  i1f0rn  25583  deg1nn0clb  25995  rgrx0ndm  29521  rgrx0nd  29522  trisecnconstr  33782  f1resfz0f1d  35101  gonan0  35379  inaex  44286  mnfnre2  45392  fonex  48855