Theorem neli 3125

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

Syntax hints:  ¬ wn 3   ∈ wcel 2114   ∉ wnel 3123

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-nel 3124

This theorem is referenced by:  alephprc  9511  pnfnre2  10669  renepnf  10675  renemnf  10676  ltxrlt  10697  nn0nepnf  11962  xrltnr  12501  pnfnlt  12510  nltmnf  12511  hashclb  13709  hasheq0  13714  egt2lt3  15544  nthruc  15590  pcgcd1  16196  pc2dvds  16198  ramtcl2  16330  nsmndex1  18061  odhash3  18684  xrsmgmdifsgrp  20565  xrsdsreclblem  20574  topnex  21587  pnfnei  21811  mnfnei  21812  zclmncvs  23735  i1f0rn  24266  deg1nn0clb  24670  rgrx0ndm  27361  rgrx0nd  27362  f1resfz0f1d  32368  gonan0  32646  inaex  40723  mnfnre2  41758