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  3740  ruOLD  3741  prneli  4608  ruv  9497  ruALT  9498  cardprc  9876  pnfnre  11156  mnfnre  11158  eirr  16114  sqrt2irr  16158  lcmfnnval  16535  lcmf0  16545  smndex1n0mnd  18786  nsmndex1  18787  zringndrg  21375  topnex  22881  zfbas  23781  aaliou3  26257  finsumvtxdg2sstep  29495  2sqr3nconstr  33754  cos9thpinconstr  33764  xrge0iifcnv  33906  bj-0nel1  36937  bj-1nel0  36938  bj-0nelsngl  36955  ruvALT  42652  fmtnoinf  47530  fmtno5nprm  47577  4fppr1  47729  gpg5edgnedg  48124  0nodd  48164  2nodd  48166  1neven  48232  2zrngnring  48252  fonex  48861  posnex  48974  prsnex  48975