Theorem nelir 3043

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

Syntax hints:  ¬ wn 3   ∈ wcel 2121   ∉ wnel 3040

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 209  df-nel 3041

This theorem is referenced by:  ru  3722  ruOLD  3723  prneli  4590  ruv  9517  ruALT  9518  cardprc  9899  pnfnre  11182  mnfnre  11184  eirr  16167  sqrt2irr  16211  lcmfnnval  16588  lcmf0  16598  smndex1n0mnd  18878  nsmndex1  18879  zringndrg  21446  topnex  22982  zfbas  23882  aaliou3  26338  finsumvtxdg2sstep  29638  ply1coedeg  33682  2sqr3nconstr  33975  cos9thpinconstr  33985  xrge0iifcnv  34127  bj-0nel1  37319  bj-1nel0  37320  bj-0nelsngl  37337  ruvALT  43132  fmtnoinf  48026  fmtno5nprm  48073  4fppr1  48238  gpg5edgnedg  48633  0nodd  48673  2nodd  48675  1neven  48741  2zrngnring  48761  fonex  49369  posnex  49482  prsnex  49483