Theorem neli 3063

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

This proof depends on syntax axioms:  ¬ wn 3   ∈ wcel 2144   ∉ wnel 3061

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-nel 3062

This theorem is used by:  alephprc  10178  pnfnre2  11351  renepnf  11357  renemnf  11358  ltxrlt  11380  nn0nepnf  12687  xrltnr  13248  pnfnlt  13257  nltmnf  13258  f1resfz0f1d  13927  hashclb  14502  hasheq0  14507  egt2lt3  16374  nthruc  16420  pcgcd1  17055  pc2dvds  17057  ramtcl2  17189  nsmndex1  19112  odhash3  19790  xrsmgmdifsgrp  21715  xrsdsreclblem  21719  topnex  23314  pnfnei  23538  mnfnei  23539  zclmncvs  25469  i1f0rn  26003  deg1nn0clb  26408  rgrx0ndm  30174  rgrx0nd  30175  nowisdomv  31075  ply1coedeg  34121  trisecnconstr  34424  gonan0  36157  inaex  45281  mnfnre2  46407  numtowerdt  47916  fonex  49977