Theorem eldifbd 3916

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2114   ∖ cdif 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906

This theorem is referenced by:  xpdifid  6136  fvdifsupp  8125  boxcutc  8893  infeq5i  9559  cantnflem2  9613  ackbij1lem18  10160  infpssrlem4  10230  fin23lem30  10266  domtriomlem  10366  pwfseqlem4  10587  dvdsaddre2b  16248  chnccats1  18562  chnccat  18563  dprdfadd  19968  pgpfac1lem2  20023  pgpfac1lem3a  20024  pgpfac1lem3  20025  lspsolv  21115  lsppratlem3  21121  frlmssuvc2  21767  mplsubrglem  21976  hauscmplem  23367  1stccnp  23423  1stckgen  23515  alexsublem  24005  bcthlem4  25300  plyeq0lem  26188  ftalem3  27058  tglngne  28640  1loopgrvd0  29596  disjiunel  32689  ofpreima2  32762  nn0difffzod  32901  gsumfs2d  33161  suppgsumssiun  33172  cycpmco2f1  33224  cycpmco2lem1  33226  cycpmco2lem5  33230  cycpmco2  33233  cyc3co2  33240  tocyccntz  33244  elrgspnlem2  33343  elrgspnlem4  33345  domnprodeq0  33376  elrspunsn  33528  mxidlmaxv  33567  mxidlirredi  33570  qsdrnglem2  33595  rprmnz  33619  rprmnunit  33620  rprmirred  33630  rprmdvdsprod  33633  1arithufdlem3  33645  dfufd2  33649  deg1prod  33682  ply1dg3rt0irred  33683  gsummoncoe1fzo  33696  evlextv  33725  psrgsum  33731  psrmonprod  33735  vieta  33763  fedgmullem2  33814  fldextrspunlsp  33858  extdgfialglem2  33877  qqhval2  34166  esum2dlem  34276  carsgclctunlem1  34501  sibfof  34524  sitgaddlemb  34532  eulerpartlemsv2  34542  eulerpartlemv  34548  eulerpartlemgs2  34564  onvf1od  35329  dochnel2  41797  evl1gprodd  42516  nelsubginvcld  42895  nelsubgcld  42896  fltne  43031  rmspecnonsq  43293  disjiun2  45447  dstregt0  45673  fprodexp  45983  fprodabs2  45984  fprodcnlem  45988  lptre2pt  46027  dvnprodlem2  46334  stoweidlem43  46430  fourierdlem66  46559  iundjiunlem  46846  hsphoidmvle2  46972  hsphoidmvle  46973  hoidmvlelem1  46982  hoidmvlelem2  46983  hoidmvlelem3  46984  hoidmvlelem4  46985  chnsubseq  47267  readdcnnred  47692  resubcnnred  47693  recnmulnred  47694  cndivrenred  47695