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  3739  ruOLD  3740  prneli  4614  ruv  9514  ruALT  9515  cardprc  9896  pnfnre  11177  mnfnre  11179  eirr  16134  sqrt2irr  16178  lcmfnnval  16555  lcmf0  16565  smndex1n0mnd  18841  nsmndex1  18842  zringndrg  21427  topnex  22944  zfbas  23844  aaliou3  26319  finsumvtxdg2sstep  29627  ply1coedeg  33672  2sqr3nconstr  33940  cos9thpinconstr  33950  xrge0iifcnv  34092  bj-0nel1  37156  bj-1nel0  37157  bj-0nelsngl  37174  ruvALT  42979  fmtnoinf  47849  fmtno5nprm  47896  4fppr1  48048  gpg5edgnedg  48443  0nodd  48483  2nodd  48485  1neven  48551  2zrngnring  48571  fonex  49179  posnex  49292  prsnex  49293