Theorem nelir 3049

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

Syntax hints:  ¬ wn 3   ∈ wcel 2106   ∉ wnel 3046

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 206  df-nel 3047

This theorem is referenced by:  ru  3775  prneli  4657  ruv  9593  ruALT  9594  cardprc  9971  pnfnre  11251  mnfnre  11253  eirr  16144  sqrt2irr  16188  lcmfnnval  16557  lcmf0  16567  smndex1n0mnd  18789  nsmndex1  18790  zringndrg  21029  topnex  22490  zfbas  23391  aaliou3  25855  finsumvtxdg2sstep  28795  xrge0iifcnv  32901  bj-0nel1  35822  bj-1nel0  35823  bj-0nelsngl  35840  ruvALT  41016  fmtnoinf  46190  fmtno5nprm  46237  4fppr1  46389  0nodd  46566  2nodd  46568  1neven  46783  2zrngnring  46803