Theorem nelir 3032

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

Syntax hints:  ¬ wn 3   ∈ wcel 2109   ∉ wnel 3029

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 3030

This theorem is referenced by:  ru  3751  ruOLD  3752  prneli  4620  ruv  9555  ruALT  9556  cardprc  9933  pnfnre  11215  mnfnre  11217  eirr  16173  sqrt2irr  16217  lcmfnnval  16594  lcmf0  16604  smndex1n0mnd  18839  nsmndex1  18840  zringndrg  21378  topnex  22883  zfbas  23783  aaliou3  26259  finsumvtxdg2sstep  29477  2sqr3nconstr  33771  cos9thpinconstr  33781  xrge0iifcnv  33923  bj-0nel1  36941  bj-1nel0  36942  bj-0nelsngl  36959  ruvALT  42657  fmtnoinf  47537  fmtno5nprm  47584  4fppr1  47736  0nodd  48158  2nodd  48160  1neven  48226  2zrngnring  48246  fonex  48855  posnex  48968  prsnex  48969