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  10028  pnfnre2  11192  renepnf  11198  renemnf  11199  ltxrlt  11220  nn0nepnf  12499  xrltnr  13055  pnfnlt  13064  nltmnf  13065  hashclb  14299  hasheq0  14304  egt2lt3  16150  nthruc  16196  pcgcd1  16824  pc2dvds  16826  ramtcl2  16958  nsmndex1  18822  odhash3  19490  xrsmgmdifsgrp  21350  xrsdsreclblem  21354  topnex  22916  pnfnei  23140  mnfnei  23141  zclmncvs  25081  i1f0rn  25616  deg1nn0clb  26028  rgrx0ndm  29574  rgrx0nd  29575  trisecnconstr  33775  f1resfz0f1d  35094  gonan0  35372  inaex  44279  mnfnre2  45385  fonex  48848