Theorem eldifbd 3926

Description: If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3923. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
eldifbd.1	⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))

Assertion

Ref	Expression
eldifbd	⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)

Proof of Theorem eldifbd

Step	Hyp	Ref	Expression
1		eldifbd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))
2		eldif 3923	. . 3 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
3	1, 2	sylib 221	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
4	3	simprd 500	1 ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∈ wcel 2149   ∖ cdif 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916

This theorem is referenced by:  xpdifid  6168  xpdifcnvepel  6169  fvdifsupp  8169  boxcutc  8941  infeq5i  9607  cantnflem2  9661  ackbij1lem18  10221  infpssrlem4  10292  fin23lem30  10328  domtriomlem  10428  pwfseqlem4  10649  dvdsaddre2b  16367  chnccats1  18683  chnccat  18684  dprdfadd  20094  pgpfac1lem2  20149  pgpfac1lem3a  20150  pgpfac1lem3  20151  lspsolv  21247  lsppratlem3  21253  prmidlsubm  21458  frlmssuvc2  21916  mplsubrglem  22124  hauscmplem  23534  1stccnp  23590  1stckgen  23682  alexsublem  24172  bcthlem4  25457  plyeq0lem  26338  ftalem3  27207  tglngne  28787  oppmir  28997  tgelrnpln  29018  elplng  29022  elplngid  29024  plngcplem  29027  plngrotlem1  29029  plngrotlem2  29030  plngrot  29032  lnssplnglem  29033  lnssplng  29034  plngmiropp  29036  nhpmirhp  29040  prlngex  29156  prlngmolem1  29157  prlngmolem2  29158  1loopgrvd0  29797  disjiunel  32884  ofpreima2  32954  nn0difffzod  33092  gsumfs2d  33324  suppgsumssiun  33335  cycpmco2f1  33387  cycpmco2lem1  33389  cycpmco2lem5  33393  cycpmco2  33396  cyc3co2  33403  tocyccntz  33407  elrgspnlem2  33506  elrgspnlem4  33508  domnprodeq0  33542  elrspunsn  33683  mxidlmaxv  33698  mxidlirredi  33701  qsdrnglem2  33725  dflringlem  33731  dflringlem2  33732  rprmnz  33757  rprmnunit  33758  rprmirred  33768  rprmdvdsprod  33771  1arithufdlem3  33783  dfufd2  33787  deg1prod  33820  ply1dg3rt0irred  33821  gsummoncoe1fzo  33834  mplidomlem  33864  evlextv  33879  psrgsum  33885  psrmonprod  33889  vieta  33917  fedgmullem2  33967  fldextrspunlsp  34011  extdgfialglem2  34030  qqhval2  34319  esum2dlem  34429  carsgclctunlem1  34654  sibfof  34677  sitgaddlemb  34685  eulerpartlemsv2  34695  eulerpartlemv  34701  eulerpartlemgs2  34717  onvf1od  35526  ttcwf2  36961  mh-inf3f1  36977  dochnel2  42093  evl1gprodd  42811  nelsubginvcld  43197  nelsubgcld  43198  fltne  43305  rmspecnonsq  43563  disjiun2  45707  dstregt0  45930  fprodexp  46239  fprodabs2  46240  fprodcnlem  46244  lptre2pt  46283  dvnprodlem2  46590  stoweidlem43  46686  fourierdlem66  46815  iundjiunlem  47102  hsphoidmvle2  47228  hsphoidmvle  47229  hoidmvlelem1  47238  hoidmvlelem2  47239  hoidmvlelem3  47240  hoidmvlelem4  47241  chnsubseq  47525  readdcnnred  47966  resubcnnred  47967  recnmulnred  47968  cndivrenred  47969