Theorem eldifbd 3918

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 400   ∈ wcel 2143   ∖ cdif 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908

This theorem is used by:  xpdifid  6165  xpdifcnvepel  6166  fvdifsupp  8163  boxcutc  8935  infeq5i  9601  cantnflem2  9655  ackbij1lem18  10224  infpssrlem4  10294  fin23lem30  10330  domtriomlem  10430  pwfseqlem4  10651  dvdsaddre2b  16369  chnccats1  18685  chnccat  18686  dprdfadd  20096  pgpfac1lem2  20151  pgpfac1lem3a  20152  pgpfac1lem3  20153  lspsolv  21276  lsppratlem3  21282  prmidlsubm  21496  frlmssuvc2  21954  mplsubrglem  22162  hauscmplem  23572  1stccnp  23628  1stckgen  23720  alexsublem  24210  bcthlem4  25495  plyeq0lem  26376  ftalem3  27248  tglngne  28828  oppmir  29045  tgelrnpln  29067  elplng  29071  elplngid  29073  plngcplem  29076  plngrotlem1  29078  plngrotlem2  29079  plngrot  29081  lnssplnglem  29082  lnssplng  29083  plngmiropp  29085  nhpmirhp  29089  prlngex  29210  prlngmolem1  29211  prlngmolem2  29212  prlngmid2  29220  1loopgrvd0  29863  disjiunel  32950  ofpreima2  33020  nn0difffzod  33158  gsumfs2d  33390  suppgsumssiun  33401  cycpmco2f1  33453  cycpmco2lem1  33455  cycpmco2lem5  33459  cycpmco2  33462  cyc3co2  33469  tocyccntz  33473  elrgspnlem2  33572  elrgspnlem4  33574  domnprodeq0  33608  elrspunsn  33746  mxidlmaxv  33760  mxidlirredi  33763  qsdrnglem2  33787  dflringlem  33793  dflringlem2  33794  rprmnz  33819  rprmnunit  33820  rprmirred  33830  rprmdvdsprod  33833  1arithufdlem3  33845  dfufd2  33849  deg1prod  33882  ply1dg3rt0irred  33883  gsummoncoe1fzo  33896  mplidomlem  33926  evlextv  33941  psrgsum  33947  psrmonprod  33951  vieta  33979  fedgmullem2  34029  fldextrspunlsp  34073  extdgfialglem2  34092  qqhval2  34381  esum2dlem  34491  carsgclctunlem1  34716  sibfof  34739  sitgaddlemb  34747  eulerpartlemsv2  34757  eulerpartlemv  34763  eulerpartlemgs2  34779  onvf1od  35599  ttcwf2  37064  mh-inf3f1  37080  dochnel2  42194  evl1gprodd  42912  nelsubginvcld  43298  nelsubgcld  43299  fltne  43404  rmspecnonsq  43662  disjiun2  45806  dstregt0  46029  fprodexp  46338  fprodabs2  46339  fprodcnlem  46343  lptre2pt  46382  dvnprodlem2  46689  stoweidlem43  46785  fourierdlem66  46914  iundjiunlem  47201  hsphoidmvle2  47327  hsphoidmvle  47328  hoidmvlelem1  47337  hoidmvlelem2  47338  hoidmvlelem3  47339  hoidmvlelem4  47340  chnsubseq  47624  readdcnnred  48068  resubcnnred  48069  recnmulnred  48070  cndivrenred  48071