Theorem nelir 3066

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

Syntax hints:  ¬ wn 3   ∈ wcel 2144   ∉ wnel 3063

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 209  df-nel 3064

This theorem is referenced by:  ru  3745  prneli  4617  ruv  9558  ruALT  9559  cardprc  9940  pnfnre  11225  mnfnre  11227  eirr  16239  sqrt2irr  16283  lcmfnnval  16660  lcmf0  16670  smndex1n0mnd  18951  nsmndex1  18952  zringndrg  21522  topnex  23058  zfbas  23958  aaliou3  26417  finsumvtxdg2sstep  29752  ply1coedeg  33787  2sqr3nconstr  34080  cos9thpinconstr  34090  xrge0iifcnv  34232  bj-0nel1  37443  bj-1nel0  37444  bj-0nelsngl  37461  ruvALT  43256  fmtnoinf  48150  fmtno5nprm  48197  4fppr1  48362  gpg5edgnedg  48757  0nodd  48797  2nodd  48799  1neven  48865  2zrngnring  48885  fonex  49493  posnex  49606  prsnex  49607