Theorem neli 3068

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

This proof depends on syntax axioms:  ¬ wn 3   ∈ wcel 2146   ∉ wnel 3066

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 3067

This theorem is used by:  alephprc  10099  pnfnre2  11268  renepnf  11274  renemnf  11275  ltxrlt  11297  nn0nepnf  12602  xrltnr  13162  pnfnlt  13171  nltmnf  13172  f1resfz0f1d  13840  hashclb  14414  hasheq0  14419  egt2lt3  16286  nthruc  16332  pcgcd1  16961  pc2dvds  16963  ramtcl2  17095  nsmndex1  19014  odhash3  19692  xrsmgmdifsgrp  21611  xrsdsreclblem  21615  topnex  23205  pnfnei  23429  mnfnei  23430  zclmncvs  25360  i1f0rn  25894  deg1nn0clb  26300  rgrx0ndm  30003  rgrx0nd  30004  nowisdomv  30898  ply1coedeg  33945  trisecnconstr  34248  gonan0  35923  inaex  45067  mnfnre2  46171  nthrucw  47667  fonex  49704