Theorem nelir 3051

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

Syntax hints:  ¬ wn 3   ∈ wcel 2108   ∉ wnel 3048

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 3049

This theorem is referenced by:  ru  3710  prneli  4588  ruv  9291  ruALT  9292  cardprc  9669  pnfnre  10947  mnfnre  10949  eirr  15842  sqrt2irr  15886  lcmfnnval  16257  lcmf0  16267  smndex1n0mnd  18466  nsmndex1  18467  zringndrg  20602  topnex  22054  zfbas  22955  aaliou3  25416  finsumvtxdg2sstep  27819  xrge0iifcnv  31785  bj-0nel1  35070  bj-1nel0  35071  bj-0nelsngl  35088  ruvALT  40096  fmtnoinf  44876  fmtno5nprm  44923  4fppr1  45075  0nodd  45252  2nodd  45254  1neven  45378  2zrngnring  45398