Theorem eldifbd 4052

Description: If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 4049. (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 4049	. . 3 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
3	1, 2	sylib 221	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
4	3	simprd 501	1 ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2144   ∖ cdif 4045

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 4047

This theorem is used by:  xpdifid  6158  xpdifcnvepel  6159  fvdifsupp  8188  boxcutc  8969  infeq5i  9637  cantnflem2  9691  ackbij1lem18  10314  infpssrlem4  10384  fin23lem30  10420  domtriomlem  10520  pwfseqlem4  10747  dvdsaddre2b  16477  chnccats1  18799  chnccat  18800  dprdfadd  20236  pgpfac1lem2  20291  pgpfac1lem3a  20292  pgpfac1lem3  20293  lspsolv  21421  lsppratlem3  21427  prmidlsubm  21643  frlmssuvc2  22101  mplsubrglem  22311  hauscmplem  23724  1stccnp  23781  1stckgen  23873  alexsublem  24363  bcthlem4  25648  plyeq0lem  26529  ftalem3  27402  fltne  27975  tglngne  29013  oppmir  29232  tgelrnpln  29254  elplng  29258  elplngid  29260  plngcplem  29263  plngrotlem1  29265  plngrotlem2  29266  plngrot  29268  lnssplnglem  29269  lnssplng  29270  plngmiropp  29272  nhpmirhp  29276  prlngex  29429  prlngmolem1  29430  prlngmolem2  29431  prlngmid2  29439  1loopgrvd0  30085  disjiunel  33190  ofpreima2  33260  nn0difffzod  33396  gsumfs2d  33622  suppgsumssiun  33633  cycpmco2f1  33685  cycpmco2lem1  33687  cycpmco2lem5  33691  cycpmco2  33694  cyc3co2  33701  tocyccntz  33705  elrgspnlem2  33804  elrgspnlem4  33806  domnprodeq0  33840  elrspunsn  33979  mxidlmaxv  33993  mxidlirredi  33996  qsdrnglem2  34020  dflringlem  34026  dflringlem2  34027  rprmnz  34052  rprmnunit  34053  rprmirred  34063  rprmdvdsprod  34066  1arithufdlem3  34078  dfufd2  34082  deg1prod  34115  ply1dg3rt0irred  34116  gsummoncoe1fzo  34129  mplidomlem  34159  evlextv  34174  psrgsum  34180  psrmonprod  34184  vieta  34212  fedgmullem2  34262  fldextrspunlsp  34306  extdgfialglem2  34325  qqhval2  34614  esum2dlem  34724  carsgclctunlem1  34949  sibfof  34972  sitgaddlemb  34980  eulerpartlemsv2  34990  eulerpartlemv  34996  eulerpartlemgs2  35012  onvf1od  35886  ttcwf2  37313  dochnel2  42450  evl1gprodd  43168  nelsubginvcld  43561  nelsubgcld  43562  rmspecnonsq  43914  disjiun2  46075  dstregt0  46298  fprodexp  46606  fprodabs2  46607  fprodcnlem  46611  lptre2pt  46650  dvnprodlem2  46957  stoweidlem43  47053  fourierdlem66  47182  iundjiunlem  47469  hsphoidmvle2  47595  hsphoidmvle  47596  hoidmvlelem1  47605  hoidmvlelem2  47606  hoidmvlelem3  47607  hoidmvlelem4  47608  readdcnnred  48373  resubcnnred  48374  recnmulnred  48375  cndivrenred  48376