Theorem nelir 3052

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

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

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 3050

This theorem is referenced by:  ru  3715  prneli  4591  ruv  9361  ruALT  9362  cardprc  9738  pnfnre  11016  mnfnre  11018  eirr  15914  sqrt2irr  15958  lcmfnnval  16329  lcmf0  16339  smndex1n0mnd  18551  nsmndex1  18552  zringndrg  20690  topnex  22146  zfbas  23047  aaliou3  25511  finsumvtxdg2sstep  27916  xrge0iifcnv  31883  bj-0nel1  35143  bj-1nel0  35144  bj-0nelsngl  35161  ruvALT  40168  fmtnoinf  44988  fmtno5nprm  45035  4fppr1  45187  0nodd  45364  2nodd  45366  1neven  45490  2zrngnring  45510