Theorem nelir 3039

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

Syntax hints:  ¬ wn 3   ∈ wcel 2112   ∉ wnel 3036

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 210  df-nel 3037

This theorem is referenced by:  ru  3682  prneli  4557  ruv  9196  ruALT  9197  cardprc  9561  pnfnre  10839  mnfnre  10841  eirr  15729  sqrt2irr  15773  lcmfnnval  16144  lcmf0  16154  smndex1n0mnd  18293  nsmndex1  18294  zringndrg  20409  topnex  21847  zfbas  22747  aaliou3  25198  finsumvtxdg2sstep  27591  xrge0iifcnv  31551  bj-0nel1  34829  bj-1nel0  34830  bj-0nelsngl  34847  ruvALT  39831  fmtnoinf  44604  fmtno5nprm  44651  4fppr1  44803  0nodd  44980  2nodd  44982  1neven  45106  2zrngnring  45126