Theorem nelir 3055

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

Syntax hints:  ¬ wn 3   ∈ wcel 2108   ∉ wnel 3052

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 3053

This theorem is referenced by:  ru  3802  ruOLD  3803  prneli  4678  ruv  9671  ruALT  9672  cardprc  10049  pnfnre  11331  mnfnre  11333  eirr  16253  sqrt2irr  16297  lcmfnnval  16671  lcmf0  16681  smndex1n0mnd  18947  nsmndex1  18948  zringndrg  21502  topnex  23024  zfbas  23925  aaliou3  26411  finsumvtxdg2sstep  29585  xrge0iifcnv  33879  bj-0nel1  36919  bj-1nel0  36920  bj-0nelsngl  36937  ruvALT  42624  fmtnoinf  47410  fmtno5nprm  47457  4fppr1  47609  0nodd  47893  2nodd  47895  1neven  47961  2zrngnring  47981