Theorem nelir 3037

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

Syntax hints:  ¬ wn 3   ∈ wcel 2113   ∉ wnel 3034

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 3035

This theorem is referenced by:  ru  3736  ruOLD  3737  prneli  4610  ruv  9501  ruALT  9502  cardprc  9883  pnfnre  11163  mnfnre  11165  eirr  16124  sqrt2irr  16168  lcmfnnval  16545  lcmf0  16555  smndex1n0mnd  18830  nsmndex1  18831  zringndrg  21415  topnex  22921  zfbas  23821  aaliou3  26296  finsumvtxdg2sstep  29539  2sqr3nconstr  33805  cos9thpinconstr  33815  xrge0iifcnv  33957  bj-0nel1  37008  bj-1nel0  37009  bj-0nelsngl  37026  ruvALT  42777  fmtnoinf  47650  fmtno5nprm  47697  4fppr1  47849  gpg5edgnedg  48244  0nodd  48284  2nodd  48286  1neven  48352  2zrngnring  48372  fonex  48981  posnex  49094  prsnex  49095