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 2144   ∉ 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  3737  prneli  4616  ruv  9602  ruALT  9603  cardprc  10061  pnfnre  11350  mnfnre  11352  eirr  16373  sqrt2irr  16417  lcmfnnval  16799  lcmf0  16809  smndex1n0mnd  19111  nsmndex1  19112  zringndrg  21774  topnex  23314  zfbas  24215  aaliou3  26678  finsumvtxdg2sstep  30130  ply1coedeg  34121  2sqr3nconstr  34413  cos9thpinconstr  34423  xrge0iifcnv  34565  bj-0nel1  37866  bj-1nel0  37867  bj-0nelsngl  37884  ruvALT  43681  fmtnoinf  48621  fmtno5nprm  48668  4fppr1  48833  gpg5edgnedg  49228  0nodd  49267  2nodd  49269  1neven  49335  2zrngnring  49355  fonex  49977  posnex  50088  prsnex  50089