Theorem nelir 3035

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

Syntax hints:  ¬ wn 3   ∈ wcel 2111   ∉ wnel 3032

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 3033

This theorem is referenced by:  ru  3734  ruOLD  3735  prneli  4606  ruv  9491  ruALT  9492  cardprc  9873  pnfnre  11153  mnfnre  11155  eirr  16114  sqrt2irr  16158  lcmfnnval  16535  lcmf0  16545  smndex1n0mnd  18820  nsmndex1  18821  zringndrg  21405  topnex  22911  zfbas  23811  aaliou3  26286  finsumvtxdg2sstep  29528  2sqr3nconstr  33794  cos9thpinconstr  33804  xrge0iifcnv  33946  bj-0nel1  36997  bj-1nel0  36998  bj-0nelsngl  37015  ruvALT  42761  fmtnoinf  47635  fmtno5nprm  47682  4fppr1  47834  gpg5edgnedg  48229  0nodd  48269  2nodd  48271  1neven  48337  2zrngnring  48357  fonex  48966  posnex  49079  prsnex  49080