Theorem nelir 3030

Description: Inference associated with df-nel 3028. (Contributed by BJ, 7-Jul-2018.)

Hypothesis

Ref	Expression
nelir.1	⊢ ¬ 𝐴 ∈ 𝐵

Assertion

Ref	Expression
nelir	⊢ 𝐴 ∉ 𝐵

Proof of Theorem nelir

Step	Hyp	Ref	Expression
1		nelir.1	. 2 ⊢ ¬ 𝐴 ∈ 𝐵
2		df-nel 3028	. 2 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)
3	1, 2	mpbir 221	1 ⊢ 𝐴 ∉ 𝐵

Syntax hints:  ¬ wn 3   ∈ wcel 2131   ∉ wnel 3027

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 197  df-nel 3028

This theorem is referenced by:  ru  3567  prneli  4339  snnexOLD  7124  ruv  8664  ruALT  8665  cardprc  8988  pnfnre  10265  mnfnre  10266  wrdlndm  13499  eirr  15124  sqrt2irr  15170  lcmfnnval  15531  lcmf0  15541  zringndrg  20032  topnex  20994  zfbas  21893  aaliou3  24297  finsumvtxdg2sstep  26647  clwwlkn0OLD  27149  xrge0iifcnv  30280  bj-0nel1  33238  bj-1nel0  33239  bj-0nelsngl  33257  fmtnoinf  41950  fmtno5nprm  41997  0nodd  42312  2nodd  42314  1neven  42434  2zrngnring  42454