Theorem eldifbd 3903

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

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

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 3432  df-dif 3893

This theorem is referenced by:  xpdifid  6128  fvdifsupp  8116  boxcutc  8884  infeq5i  9552  cantnflem2  9606  ackbij1lem18  10153  infpssrlem4  10223  fin23lem30  10259  domtriomlem  10359  pwfseqlem4  10580  dvdsaddre2b  16271  chnccats1  18586  chnccat  18587  dprdfadd  19992  pgpfac1lem2  20047  pgpfac1lem3a  20048  pgpfac1lem3  20049  lspsolv  21137  lsppratlem3  21143  frlmssuvc2  21789  mplsubrglem  21996  hauscmplem  23385  1stccnp  23441  1stckgen  23533  alexsublem  24023  bcthlem4  25308  plyeq0lem  26189  ftalem3  27056  tglngne  28636  1loopgrvd0  29592  disjiunel  32685  ofpreima2  32758  nn0difffzod  32896  gsumfs2d  33141  suppgsumssiun  33152  cycpmco2f1  33204  cycpmco2lem1  33206  cycpmco2lem5  33210  cycpmco2  33213  cyc3co2  33220  tocyccntz  33224  elrgspnlem2  33323  elrgspnlem4  33325  domnprodeq0  33356  elrspunsn  33508  mxidlmaxv  33547  mxidlirredi  33550  qsdrnglem2  33575  rprmnz  33599  rprmnunit  33600  rprmirred  33610  rprmdvdsprod  33613  1arithufdlem3  33625  dfufd2  33629  deg1prod  33662  ply1dg3rt0irred  33663  gsummoncoe1fzo  33676  evlextv  33705  psrgsum  33711  psrmonprod  33715  vieta  33743  fedgmullem2  33794  fldextrspunlsp  33838  extdgfialglem2  33857  qqhval2  34146  esum2dlem  34256  carsgclctunlem1  34481  sibfof  34504  sitgaddlemb  34512  eulerpartlemsv2  34522  eulerpartlemv  34528  eulerpartlemgs2  34544  onvf1od  35309  ttcwf2  36727  mh-inf3f1  36743  dochnel2  41856  evl1gprodd  42574  nelsubginvcld  42959  nelsubgcld  42960  fltne  43095  rmspecnonsq  43357  disjiun2  45511  dstregt0  45737  fprodexp  46046  fprodabs2  46047  fprodcnlem  46051  lptre2pt  46090  dvnprodlem2  46397  stoweidlem43  46493  fourierdlem66  46622  iundjiunlem  46909  hsphoidmvle2  47035  hsphoidmvle  47036  hoidmvlelem1  47045  hoidmvlelem2  47046  hoidmvlelem3  47047  hoidmvlelem4  47048  chnsubseq  47330  readdcnnred  47767  resubcnnred  47768  recnmulnred  47769  cndivrenred  47770