Theorem nelir 3049

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

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

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 3047

This theorem is referenced by:  ru  3786  ruOLD  3787  prneli  4656  ruv  9642  ruALT  9643  cardprc  10020  pnfnre  11302  mnfnre  11304  eirr  16241  sqrt2irr  16285  lcmfnnval  16661  lcmf0  16671  smndex1n0mnd  18925  nsmndex1  18926  zringndrg  21479  topnex  23003  zfbas  23904  aaliou3  26393  finsumvtxdg2sstep  29567  xrge0iifcnv  33932  bj-0nel1  36954  bj-1nel0  36955  bj-0nelsngl  36972  ruvALT  42679  fmtnoinf  47523  fmtno5nprm  47570  4fppr1  47722  0nodd  48086  2nodd  48088  1neven  48154  2zrngnring  48174