Theorem nelir 3044

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

Syntax hints:  ¬ wn 3   ∈ wcel 2099   ∉ wnel 3041

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 3042

This theorem is referenced by:  ru  3773  prneli  4654  ruv  9617  ruALT  9618  cardprc  9995  pnfnre  11277  mnfnre  11279  eirr  16173  sqrt2irr  16217  lcmfnnval  16586  lcmf0  16596  smndex1n0mnd  18855  nsmndex1  18856  zringndrg  21381  topnex  22886  zfbas  23787  aaliou3  26273  finsumvtxdg2sstep  29350  xrge0iifcnv  33470  bj-0nel1  36368  bj-1nel0  36369  bj-0nelsngl  36386  ruvALT  42015  fmtnoinf  46799  fmtno5nprm  46846  4fppr1  46998  0nodd  47155  2nodd  47157  1neven  47223  2zrngnring  47243