Theorem nelir 3037

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

Syntax hints:  ¬ wn 3   ∈ wcel 2113   ∉ wnel 3034

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 3035

This theorem is referenced by:  ru  3736  ruOLD  3737  prneli  4611  ruv  9508  ruALT  9509  cardprc  9890  pnfnre  11171  mnfnre  11173  eirr  16128  sqrt2irr  16172  lcmfnnval  16549  lcmf0  16559  smndex1n0mnd  18835  nsmndex1  18836  zringndrg  21421  topnex  22938  zfbas  23838  aaliou3  26313  finsumvtxdg2sstep  29572  ply1coedeg  33619  2sqr3nconstr  33887  cos9thpinconstr  33897  xrge0iifcnv  34039  bj-0nel1  37097  bj-1nel0  37098  bj-0nelsngl  37115  ruvALT  42854  fmtnoinf  47724  fmtno5nprm  47771  4fppr1  47923  gpg5edgnedg  48318  0nodd  48358  2nodd  48360  1neven  48426  2zrngnring  48446  fonex  49054  posnex  49167  prsnex  49168