Theorem eldifbd 3910

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900

This theorem is referenced by:  xpdifid  6115  fvdifsupp  8101  boxcutc  8865  infeq5i  9526  cantnflem2  9580  ackbij1lem18  10127  infpssrlem4  10197  fin23lem30  10233  domtriomlem  10333  pwfseqlem4  10553  dvdsaddre2b  16218  chnccats1  18531  chnccat  18532  dprdfadd  19934  pgpfac1lem2  19989  pgpfac1lem3a  19990  pgpfac1lem3  19991  lspsolv  21080  lsppratlem3  21086  frlmssuvc2  21732  mplsubrglem  21941  hauscmplem  23321  1stccnp  23377  1stckgen  23469  alexsublem  23959  bcthlem4  25254  plyeq0lem  26142  ftalem3  27012  tglngne  28528  1loopgrvd0  29483  disjiunel  32576  ofpreima2  32648  nn0difffzod  32786  gsumfs2d  33035  cycpmco2f1  33093  cycpmco2lem1  33095  cycpmco2lem5  33099  cycpmco2  33102  cyc3co2  33109  tocyccntz  33113  elrgspnlem2  33210  elrgspnlem4  33212  elrspunsn  33394  mxidlmaxv  33433  mxidlirredi  33436  qsdrnglem2  33461  rprmnz  33485  rprmnunit  33486  rprmirred  33496  rprmdvdsprod  33499  1arithufdlem3  33511  dfufd2  33515  ply1dg3rt0irred  33546  gsummoncoe1fzo  33558  fedgmullem2  33643  fldextrspunlsp  33687  extdgfialglem2  33706  qqhval2  33995  esum2dlem  34105  carsgclctunlem1  34330  sibfof  34353  sitgaddlemb  34361  eulerpartlemsv2  34371  eulerpartlemv  34377  eulerpartlemgs2  34393  onvf1od  35151  dochnel2  41490  evl1gprodd  42209  nelsubginvcld  42588  nelsubgcld  42589  fltne  42736  rmspecnonsq  42999  disjiun2  45154  dstregt0  45382  fprodexp  45693  fprodabs2  45694  fprodcnlem  45698  lptre2pt  45737  dvnprodlem2  46044  stoweidlem43  46140  fourierdlem66  46269  iundjiunlem  46556  hsphoidmvle2  46682  hsphoidmvle  46683  hoidmvlelem1  46692  hoidmvlelem2  46693  hoidmvlelem3  46694  hoidmvlelem4  46695  chnsubseq  46977  readdcnnred  47402  resubcnnred  47403  recnmulnred  47404  cndivrenred  47405