Theorem neli 3032

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

Syntax hints:  ¬ wn 3   ∈ wcel 2109   ∉ wnel 3030

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 207  df-nel 3031

This theorem is referenced by:  alephprc  10059  pnfnre2  11223  renepnf  11229  renemnf  11230  ltxrlt  11251  nn0nepnf  12530  xrltnr  13086  pnfnlt  13095  nltmnf  13096  hashclb  14330  hasheq0  14335  egt2lt3  16181  nthruc  16227  pcgcd1  16855  pc2dvds  16857  ramtcl2  16989  nsmndex1  18847  odhash3  19513  xrsmgmdifsgrp  21327  xrsdsreclblem  21336  topnex  22890  pnfnei  23114  mnfnei  23115  zclmncvs  25055  i1f0rn  25590  deg1nn0clb  26002  rgrx0ndm  29528  rgrx0nd  29529  trisecnconstr  33789  f1resfz0f1d  35108  gonan0  35386  inaex  44293  mnfnre2  45399  fonex  48859