Theorem nelir 2886

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

Syntax hints:  ¬ wn 3   ∈ wcel 1977   ∉ wnel 2781

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 196  df-nel 2783

This theorem is referenced by:  ru  3401  prneli  4150  snnex  6862  ruv  8390  ruALT  8391  cardprc  8689  pnfnre  9960  mnfnre  9961  wrdlndm  13176  eirr  14772  sqrt2irr  14817  lcmfnnval  15175  lcmf0  15185  zringndrg  19657  zfbas  21510  aaliou3  23910  xrge0iifcnv  29307  bj-0nel1  32133  bj-1nel0  32134  bj-0nelsngl  32152  bj-topnex  32247  fmtnoinf  39986  fmtno5nprm  40033  clwwlksn0  41214  0nodd  41600  2nodd  41602  1neven  41722  2zrngnring  41742