Theorem neli 3067

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

This proof depends on syntax axioms:  ¬ wn 3   ∈ wcel 2147   ∉ wnel 3065

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 3066

This theorem is used by:  alephprc  10202  pnfnre2  11375  renepnf  11381  renemnf  11382  ltxrlt  11404  nn0nepnf  12711  xrltnr  13272  pnfnlt  13281  nltmnf  13282  f1resfz0f1d  13951  hashclb  14526  hasheq0  14531  egt2lt3  16400  nthruc  16446  pcgcd1  17081  pc2dvds  17083  ramtcl2  17215  nsmndex1  19138  odhash3  19817  xrsmgmdifsgrp  21742  xrsdsreclblem  21746  topnex  23341  pnfnei  23565  mnfnei  23566  zclmncvs  25496  i1f0rn  26030  deg1nn0clb  26435  rgrx0ndm  30201  rgrx0nd  30202  nowisdomv  31102  ply1coedeg  34188  trisecnconstr  34491  gonan0  36323  inaex  45471  mnfnre2  46610  numtowerdt  48119  fonex  50181