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 2108   ∉ 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  3763  ruOLD  3764  prneli  4632  ruv  9614  ruALT  9615  cardprc  9992  pnfnre  11274  mnfnre  11276  eirr  16221  sqrt2irr  16265  lcmfnnval  16641  lcmf0  16651  smndex1n0mnd  18888  nsmndex1  18889  zringndrg  21427  topnex  22932  zfbas  23832  aaliou3  26309  finsumvtxdg2sstep  29475  2sqr3nconstr  33761  xrge0iifcnv  33910  bj-0nel1  36917  bj-1nel0  36918  bj-0nelsngl  36935  ruvALT  42639  fmtnoinf  47498  fmtno5nprm  47545  4fppr1  47697  0nodd  48093  2nodd  48095  1neven  48161  2zrngnring  48181  fonex  48790  posnex  48902  prsnex  48903