Theorem nelir 3039

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

Syntax hints:  ¬ wn 3   ∈ wcel 2114   ∉ wnel 3036

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 3037

This theorem is referenced by:  ru  3726  ruOLD  3727  prneli  4600  ruv  9522  ruALT  9523  cardprc  9904  pnfnre  11186  mnfnre  11188  eirr  16172  sqrt2irr  16216  lcmfnnval  16593  lcmf0  16603  smndex1n0mnd  18883  nsmndex1  18884  zringndrg  21448  topnex  22961  zfbas  23861  aaliou3  26317  finsumvtxdg2sstep  29618  ply1coedeg  33649  2sqr3nconstr  33925  cos9thpinconstr  33935  xrge0iifcnv  34077  bj-0nel1  37260  bj-1nel0  37261  bj-0nelsngl  37278  ruvALT  43102  fmtnoinf  47999  fmtno5nprm  48046  4fppr1  48211  gpg5edgnedg  48606  0nodd  48646  2nodd  48648  1neven  48714  2zrngnring  48734  fonex  49342  posnex  49455  prsnex  49456