Theorem nelir 3065

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

Syntax hints:  ¬ wn 3   ∈ wcel 2141   ∉ wnel 3062

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 210  df-nel 3063

This theorem is referenced by:  ru  3742  prneli  4621  ruv  9569  ruALT  9570  cardprc  9965  pnfnre  11249  mnfnre  11251  eirr  16260  sqrt2irr  16304  lcmfnnval  16681  lcmf0  16691  smndex1n0mnd  18973  nsmndex1  18974  zringndrg  21597  topnex  23132  zfbas  24032  aaliou3  26491  finsumvtxdg2sstep  29865  ply1coedeg  33845  2sqr3nconstr  34137  cos9thpinconstr  34147  xrge0iifcnv  34289  bj-0nel1  37533  bj-1nel0  37534  bj-0nelsngl  37551  ruvALT  43349  fmtnoinf  48233  fmtno5nprm  48280  4fppr1  48445  gpg5edgnedg  48840  0nodd  48880  2nodd  48882  1neven  48948  2zrngnring  48968  fonex  49590  posnex  49703  prsnex  49704