Theorem neli 3046

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

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

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 3045

This theorem is referenced by:  alephprc  10137  pnfnre2  11301  renepnf  11307  renemnf  11308  ltxrlt  11329  nn0nepnf  12605  xrltnr  13159  pnfnlt  13168  nltmnf  13169  hashclb  14394  hasheq0  14399  egt2lt3  16239  nthruc  16285  pcgcd1  16911  pc2dvds  16913  ramtcl2  17045  nsmndex1  18939  odhash3  19609  xrsmgmdifsgrp  21439  xrsdsreclblem  21448  topnex  23019  pnfnei  23244  mnfnei  23245  zclmncvs  25196  i1f0rn  25731  deg1nn0clb  26144  rgrx0ndm  29626  rgrx0nd  29627  f1resfz0f1d  35098  gonan0  35377  inaex  44293  mnfnre2  45346