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 2145   ∉ 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  10127  pnfnre2  11300  renepnf  11306  renemnf  11307  ltxrlt  11329  nn0nepnf  12634  xrltnr  13195  pnfnlt  13204  nltmnf  13205  f1resfz0f1d  13873  hashclb  14447  hasheq0  14452  egt2lt3  16319  nthruc  16365  pcgcd1  16994  pc2dvds  16996  ramtcl2  17128  nsmndex1  19051  odhash3  19729  xrsmgmdifsgrp  21654  xrsdsreclblem  21658  topnex  23253  pnfnei  23477  mnfnei  23478  zclmncvs  25408  i1f0rn  25942  deg1nn0clb  26347  rgrx0ndm  30085  rgrx0nd  30086  nowisdomv  30986  ply1coedeg  34032  trisecnconstr  34335  gonan0  36054  inaex  45186  mnfnre2  46290  numtowerdt  47799  fonex  49860