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 232	1 ⊢ ¬ 𝐴 ∈ 𝐵

Syntax hints:  ¬ wn 3   ∈ wcel 2142   ∉ wnel 3061

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 3062

This theorem is referenced by:  alephprc  10055  pnfnre2  11224  renepnf  11230  renemnf  11231  ltxrlt  11253  nn0nepnf  12562  xrltnr  13121  pnfnlt  13130  nltmnf  13131  hashclb  14371  hasheq0  14376  egt2lt3  16238  nthruc  16284  pcgcd1  16913  pc2dvds  16915  ramtcl2  17047  nsmndex1  18950  odhash3  19616  xrsmgmdifsgrp  21461  xrsdsreclblem  21465  topnex  23056  pnfnei  23280  mnfnei  23281  zclmncvs  25210  i1f0rn  25744  deg1nn0clb  26150  rgrx0ndm  29794  rgrx0nd  29795  nowisdomv  30676  ply1coedeg  33785  trisecnconstr  34089  f1resfz0f1d  35464  gonan0  35742  inaex  44873  mnfnre2  45971  fonex  49488