Theorem nelir 3066

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

This proof depends on syntax axioms:  ¬ wn 3   ∈ wcel 2145   ∉ wnel 3063

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-nel 3064

This theorem is used by:  ru  3741  prneli  4620  ruv  9583  ruALT  9584  cardprc  9988  pnfnre  11277  mnfnre  11279  eirr  16297  sqrt2irr  16341  lcmfnnval  16718  lcmf0  16728  smndex1n0mnd  19025  nsmndex1  19026  zringndrg  21682  topnex  23222  zfbas  24123  aaliou3  26584  finsumvtxdg2sstep  29995  ply1coedeg  33986  2sqr3nconstr  34278  cos9thpinconstr  34288  xrge0iifcnv  34430  bj-0nel1  37684  bj-1nel0  37685  bj-0nelsngl  37702  ruvALT  43502  fmtnoinf  48426  fmtno5nprm  48473  4fppr1  48638  gpg5edgnedg  49033  0nodd  49072  2nodd  49074  1neven  49140  2zrngnring  49160  fonex  49782  posnex  49893  prsnex  49894