Theorem nelir 3046

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

Syntax hints:  ¬ wn 3   ∈ wcel 2105   ∉ wnel 3043

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 207  df-nel 3044

This theorem is referenced by:  ru  3788  ruOLD  3789  prneli  4660  ruv  9639  ruALT  9640  cardprc  10017  pnfnre  11299  mnfnre  11301  eirr  16237  sqrt2irr  16281  lcmfnnval  16657  lcmf0  16667  smndex1n0mnd  18937  nsmndex1  18938  zringndrg  21496  topnex  23018  zfbas  23919  aaliou3  26407  finsumvtxdg2sstep  29581  xrge0iifcnv  33893  bj-0nel1  36935  bj-1nel0  36936  bj-0nelsngl  36953  ruvALT  42655  fmtnoinf  47460  fmtno5nprm  47507  4fppr1  47659  0nodd  48013  2nodd  48015  1neven  48081  2zrngnring  48101