Theorem nelir 3126

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

Syntax hints:  ¬ wn 3   ∈ wcel 2110   ∉ wnel 3123

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 209  df-nel 3124

This theorem is referenced by:  ru  3770  prneli  4588  ruv  9060  ruALT  9061  cardprc  9403  pnfnre  10676  mnfnre  10678  wrdlndmOLD  13874  eirr  15552  sqrt2irr  15596  lcmfnnval  15962  lcmf0  15972  smndex1n0mnd  18071  nsmndex1  18072  zringndrg  20631  topnex  21598  zfbas  22498  aaliou3  24934  finsumvtxdg2sstep  27325  xrge0iifcnv  31171  bj-0nel1  34260  bj-1nel0  34261  bj-0nelsngl  34278  fmtnoinf  43692  fmtno5nprm  43739  4fppr1  43894  0nodd  44071  2nodd  44073  1neven  44197  2zrngnring  44217