Theorem nelir 3091

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

Syntax hints:  ¬ wn 3   ∈ wcel 2079   ∉ wnel 3088

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 208  df-nel 3089

This theorem is referenced by:  ru  3700  prneli  4494  ruv  8902  ruALT  8903  cardprc  9244  pnfnre  10517  mnfnre  10519  wrdlndmOLD  13714  eirr  15379  sqrt2irr  15423  lcmfnnval  15785  lcmf0  15795  zringndrg  20307  topnex  21276  zfbas  22176  aaliou3  24611  finsumvtxdg2sstep  27002  xrge0iifcnv  30749  bj-0nel1  33782  bj-1nel0  33783  bj-0nelsngl  33834  fmtnoinf  43134  fmtno5nprm  43181  4fppr1  43336  0nodd  43513  2nodd  43515  1neven  43635  2zrngnring  43655