Theorem nelir 3064

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

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

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 3062

This theorem is used by:  ru  3738  prneli  4617  ruv  9580  ruALT  9581  cardprc  10018  pnfnre  11307  mnfnre  11309  eirr  16326  sqrt2irr  16370  lcmfnnval  16747  lcmf0  16757  smndex1n0mnd  19058  nsmndex1  19059  zringndrg  21721  topnex  23261  zfbas  24162  aaliou3  26627  finsumvtxdg2sstep  30049  ply1coedeg  34040  2sqr3nconstr  34332  cos9thpinconstr  34342  xrge0iifcnv  34484  bj-0nel1  37782  bj-1nel0  37783  bj-0nelsngl  37800  ruvALT  43613  fmtnoinf  48537  fmtno5nprm  48584  4fppr1  48749  gpg5edgnedg  49144  0nodd  49183  2nodd  49185  1neven  49251  2zrngnring  49271  fonex  49893  posnex  50004  prsnex  50005