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 2114   ∉ 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  3771  prneli  4595  ruv  9066  ruALT  9067  cardprc  9409  pnfnre  10682  mnfnre  10684  wrdlndmOLD  13880  eirr  15558  sqrt2irr  15602  lcmfnnval  15968  lcmf0  15978  smndex1n0mnd  18077  nsmndex1  18078  zringndrg  20637  topnex  21604  zfbas  22504  aaliou3  24940  finsumvtxdg2sstep  27331  xrge0iifcnv  31176  bj-0nel1  34268  bj-1nel0  34269  bj-0nelsngl  34286  fmtnoinf  43718  fmtno5nprm  43765  4fppr1  43920  0nodd  44097  2nodd  44099  1neven  44223  2zrngnring  44243