Theorem nelir 3033

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

Syntax hints:  ¬ wn 3   ∈ wcel 2109   ∉ wnel 3030

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 3031

This theorem is referenced by:  ru  3754  ruOLD  3755  prneli  4623  ruv  9562  ruALT  9563  cardprc  9940  pnfnre  11222  mnfnre  11224  eirr  16180  sqrt2irr  16224  lcmfnnval  16601  lcmf0  16611  smndex1n0mnd  18846  nsmndex1  18847  zringndrg  21385  topnex  22890  zfbas  23790  aaliou3  26266  finsumvtxdg2sstep  29484  2sqr3nconstr  33778  cos9thpinconstr  33788  xrge0iifcnv  33930  bj-0nel1  36948  bj-1nel0  36949  bj-0nelsngl  36966  ruvALT  42664  fmtnoinf  47541  fmtno5nprm  47588  4fppr1  47740  0nodd  48162  2nodd  48164  1neven  48230  2zrngnring  48250  fonex  48859  posnex  48972  prsnex  48973