Theorem nelir 3068

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

This proof depends on syntax axioms:  ¬ wn 3   ∈ wcel 2147   ∉ wnel 3065

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 3066

This theorem is used by:  ru  3741  prneli  4617  ruv  9626  ruALT  9627  cardprc  10085  pnfnre  11374  mnfnre  11376  eirr  16399  sqrt2irr  16443  lcmfnnval  16825  lcmf0  16835  smndex1n0mnd  19137  nsmndex1  19138  zringndrg  21801  topnex  23341  zfbas  24242  aaliou3  26705  finsumvtxdg2sstep  30157  ply1coedeg  34188  2sqr3nconstr  34480  cos9thpinconstr  34490  xrge0iifcnv  34632  mirimanoffr  36626  mirimanofffr  36628  cardprcALT  36633  bj-0nel1  38043  bj-1nel0  38044  bj-0nelsngl  38061  ruvALT  43871  fmtnoinf  48824  fmtno5nprm  48871  4fppr1  49036  gpg5edgnedg  49431  0nodd  49470  2nodd  49472  1neven  49538  2zrngnring  49558  fonex  50181  posnex  50297  prsnex  50298