Theorem nelir 3050

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

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

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 3048

This theorem is referenced by:  ru  3729  prneli  4607  ruv  9463  ruALT  9464  cardprc  9841  pnfnre  11121  mnfnre  11123  eirr  16013  sqrt2irr  16057  lcmfnnval  16426  lcmf0  16436  smndex1n0mnd  18647  nsmndex1  18648  zringndrg  20795  topnex  22251  zfbas  23152  aaliou3  25616  finsumvtxdg2sstep  28204  xrge0iifcnv  32179  bj-0nel1  35278  bj-1nel0  35279  bj-0nelsngl  35296  ruvALT  40476  fmtnoinf  45406  fmtno5nprm  45453  4fppr1  45605  0nodd  45782  2nodd  45784  1neven  45908  2zrngnring  45928