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 2142   ∉ 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  3742  prneli  4621  ruv  9568  ruALT  9569  cardprc  9973  pnfnre  11256  mnfnre  11258  eirr  16267  sqrt2irr  16311  lcmfnnval  16688  lcmf0  16698  smndex1n0mnd  18980  nsmndex1  18981  zringndrg  21629  topnex  23164  zfbas  24064  aaliou3  26525  finsumvtxdg2sstep  29910  ply1coedeg  33888  2sqr3nconstr  34180  cos9thpinconstr  34190  xrge0iifcnv  34332  bj-0nel1  37617  bj-1nel0  37618  bj-0nelsngl  37635  ruvALT  43429  fmtnoinf  48316  fmtno5nprm  48363  4fppr1  48528  gpg5edgnedg  48923  0nodd  48963  2nodd  48965  1neven  49031  2zrngnring  49051  fonex  49673  posnex  49786  prsnex  49787