Theorem eldifbd 3964

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954

This theorem is referenced by:  xpdifid  6188  fvdifsupp  8196  boxcutc  8981  infeq5i  9676  cantnflem2  9730  ackbij1lem18  10276  infpssrlem4  10346  fin23lem30  10382  domtriomlem  10482  pwfseqlem4  10702  dvdsaddre2b  16344  dprdfadd  20040  pgpfac1lem2  20095  pgpfac1lem3a  20096  pgpfac1lem3  20097  lspsolv  21145  lsppratlem3  21151  frlmssuvc2  21815  mplsubrglem  22024  hauscmplem  23414  1stccnp  23470  1stckgen  23562  alexsublem  24052  bcthlem4  25361  plyeq0lem  26249  ftalem3  27118  tglngne  28558  1loopgrvd0  29522  disjiunel  32609  ofpreima2  32676  nn0difffzod  32808  chnccats1  33005  gsumfs2d  33058  cycpmco2f1  33144  cycpmco2lem1  33146  cycpmco2lem5  33150  cycpmco2  33153  cyc3co2  33160  tocyccntz  33164  elrgspnlem2  33247  elrgspnlem4  33249  elrspunsn  33457  mxidlmaxv  33496  mxidlirredi  33499  qsdrnglem2  33524  rprmnz  33548  rprmnunit  33549  rprmirred  33559  rprmdvdsprod  33562  1arithufdlem3  33574  dfufd2  33578  ply1dg3rt0irred  33607  gsummoncoe1fzo  33618  fedgmullem2  33681  fldextrspunlsp  33724  qqhval2  33983  esum2dlem  34093  carsgclctunlem1  34319  sibfof  34342  sitgaddlemb  34350  eulerpartlemsv2  34360  eulerpartlemv  34366  eulerpartlemgs2  34382  dochnel2  41394  evl1gprodd  42118  nelsubginvcld  42506  nelsubgcld  42507  fltne  42654  rmspecnonsq  42918  disjiun2  45063  dstregt0  45293  fprodexp  45609  fprodabs2  45610  fprodcnlem  45614  lptre2pt  45655  dvnprodlem2  45962  stoweidlem43  46058  fourierdlem66  46187  iundjiunlem  46474  hsphoidmvle2  46600  hsphoidmvle  46601  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem4  46613  readdcnnred  47315  resubcnnred  47316  recnmulnred  47317  cndivrenred  47318