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  11270  renepnf  11276  renemnf  11277  ltxrlt  11299  nn0nepnf  12604  xrltnr  13164  pnfnlt  13173  nltmnf  13174  f1resfz0f1d  13842  hashclb  14416  hasheq0  14421  egt2lt3  16288  nthruc  16334  pcgcd1  16963  pc2dvds  16965  ramtcl2  17097  nsmndex1  19016  odhash3  19694  xrsmgmdifsgrp  21613  xrsdsreclblem  21617  topnex  23207  pnfnei  23431  mnfnei  23432  zclmncvs  25362  i1f0rn  25896  deg1nn0clb  26302  rgrx0ndm  30005  rgrx0nd  30006  nowisdomv  30900  ply1coedeg  33947  trisecnconstr  34250  gonan0  35925  inaex  45084  mnfnre2  46188  nthrucw  47684  fonex  49721