Theorem nelir 3047

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

Syntax hints:  ¬ wn 3   ∈ wcel 2104   ∉ 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 206  df-nel 3045

This theorem is referenced by:  ru  3777  prneli  4659  ruv  9601  ruALT  9602  cardprc  9979  pnfnre  11261  mnfnre  11263  eirr  16154  sqrt2irr  16198  lcmfnnval  16567  lcmf0  16577  smndex1n0mnd  18831  nsmndex1  18832  zringndrg  21241  topnex  22721  zfbas  23622  aaliou3  26098  finsumvtxdg2sstep  29071  xrge0iifcnv  33209  bj-0nel1  36139  bj-1nel0  36140  bj-0nelsngl  36157  ruvALT  41715  fmtnoinf  46504  fmtno5nprm  46551  4fppr1  46703  0nodd  46848  2nodd  46850  1neven  46920  2zrngnring  46940