Theorem neli 3050

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

Syntax hints:  ¬ wn 3   ∈ wcel 2108   ∉ wnel 3048

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 3049

This theorem is referenced by:  alephprc  9786  pnfnre2  10948  renepnf  10954  renemnf  10955  ltxrlt  10976  nn0nepnf  12243  xrltnr  12784  pnfnlt  12793  nltmnf  12794  hashclb  14001  hasheq0  14006  egt2lt3  15843  nthruc  15889  pcgcd1  16506  pc2dvds  16508  ramtcl2  16640  nsmndex1  18467  odhash3  19096  xrsmgmdifsgrp  20547  xrsdsreclblem  20556  topnex  22054  pnfnei  22279  mnfnei  22280  zclmncvs  24217  i1f0rn  24751  deg1nn0clb  25160  rgrx0ndm  27863  rgrx0nd  27864  f1resfz0f1d  32972  gonan0  33254  inaex  41804  mnfnre2  42826