Theorem nelir 3040

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

Syntax hints:  ¬ wn 3   ∈ wcel 2114   ∉ wnel 3037

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 207  df-nel 3038

This theorem is referenced by:  ru  3727  ruOLD  3728  prneli  4601  ruv  9517  ruALT  9518  cardprc  9899  pnfnre  11181  mnfnre  11183  eirr  16167  sqrt2irr  16211  lcmfnnval  16588  lcmf0  16598  smndex1n0mnd  18878  nsmndex1  18879  zringndrg  21462  topnex  22975  zfbas  23875  aaliou3  26332  finsumvtxdg2sstep  29637  ply1coedeg  33668  2sqr3nconstr  33945  cos9thpinconstr  33955  xrge0iifcnv  34097  bj-0nel1  37280  bj-1nel0  37281  bj-0nelsngl  37298  ruvALT  43120  fmtnoinf  48015  fmtno5nprm  48062  4fppr1  48227  gpg5edgnedg  48622  0nodd  48662  2nodd  48664  1neven  48730  2zrngnring  48750  fonex  49358  posnex  49471  prsnex  49472