Theorem neli 3047

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

Syntax hints:  ¬ wn 3   ∈ wcel 2105   ∉ wnel 3045

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 3046

This theorem is referenced by:  alephprc  10100  pnfnre2  11263  renepnf  11269  renemnf  11270  ltxrlt  11291  nn0nepnf  12559  xrltnr  13106  pnfnlt  13115  nltmnf  13116  hashclb  14325  hasheq0  14330  egt2lt3  16156  nthruc  16202  pcgcd1  16817  pc2dvds  16819  ramtcl2  16951  nsmndex1  18836  odhash3  19492  xrsmgmdifsgrp  21270  xrsdsreclblem  21279  topnex  22818  pnfnei  23043  mnfnei  23044  zclmncvs  24995  i1f0rn  25530  deg1nn0clb  25945  rgrx0ndm  29282  rgrx0nd  29283  f1resfz0f1d  34566  gonan0  34846  inaex  43518  mnfnre2  44564