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  3748  ruOLD  3749  prneli  4616  ruv  9531  ruALT  9532  cardprc  9909  pnfnre  11191  mnfnre  11193  eirr  16149  sqrt2irr  16193  lcmfnnval  16570  lcmf0  16580  smndex1n0mnd  18821  nsmndex1  18822  zringndrg  21410  topnex  22916  zfbas  23816  aaliou3  26292  finsumvtxdg2sstep  29530  2sqr3nconstr  33764  cos9thpinconstr  33774  xrge0iifcnv  33916  bj-0nel1  36934  bj-1nel0  36935  bj-0nelsngl  36952  ruvALT  42650  fmtnoinf  47530  fmtno5nprm  47577  4fppr1  47729  0nodd  48151  2nodd  48153  1neven  48219  2zrngnring  48239  fonex  48848  posnex  48961  prsnex  48962