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  3740  ruOLD  3741  prneli  4615  ruv  9524  ruALT  9525  cardprc  9906  pnfnre  11187  mnfnre  11189  eirr  16144  sqrt2irr  16188  lcmfnnval  16565  lcmf0  16575  smndex1n0mnd  18854  nsmndex1  18855  zringndrg  21440  topnex  22957  zfbas  23857  aaliou3  26332  finsumvtxdg2sstep  29641  ply1coedeg  33688  2sqr3nconstr  33965  cos9thpinconstr  33975  xrge0iifcnv  34117  bj-0nel1  37228  bj-1nel0  37229  bj-0nelsngl  37246  ruvALT  43056  fmtnoinf  47925  fmtno5nprm  47972  4fppr1  48124  gpg5edgnedg  48519  0nodd  48559  2nodd  48561  1neven  48627  2zrngnring  48647  fonex  49255  posnex  49368  prsnex  49369