Theorem neli 3048

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

Syntax hints:  ¬ wn 3   ∈ wcel 2106   ∉ wnel 3046

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 206  df-nel 3047

This theorem is referenced by:  alephprc  10090  pnfnre2  11252  renepnf  11258  renemnf  11259  ltxrlt  11280  nn0nepnf  12548  xrltnr  13095  pnfnlt  13104  nltmnf  13105  hashclb  14314  hasheq0  14319  egt2lt3  16145  nthruc  16191  pcgcd1  16806  pc2dvds  16808  ramtcl2  16940  nsmndex1  18790  odhash3  19438  xrsmgmdifsgrp  20974  xrsdsreclblem  20983  topnex  22490  pnfnei  22715  mnfnei  22716  zclmncvs  24656  i1f0rn  25190  deg1nn0clb  25599  rgrx0ndm  28839  rgrx0nd  28840  f1resfz0f1d  34091  gonan0  34371  inaex  43041  mnfnre2  44092