Theorem eldifbd 3948

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∈ wcel 2110   ∖ cdif 3932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3938

This theorem is referenced by:  xpdifid  6024  boxcutc  8504  infeq5i  9098  cantnflem2  9152  ackbij1lem18  9658  infpssrlem4  9727  fin23lem30  9763  domtriomlem  9863  pwfseqlem4  10083  dvdsaddre2b  15656  dprdfadd  19141  pgpfac1lem2  19196  pgpfac1lem3a  19197  pgpfac1lem3  19198  lspsolv  19914  lsppratlem3  19920  mplsubrglem  20218  frlmssuvc2  20938  hauscmplem  22013  1stccnp  22069  1stckgen  22161  alexsublem  22651  bcthlem4  23929  plyeq0lem  24799  ftalem3  25651  tglngne  26335  1loopgrvd0  27285  disjiunel  30345  ofpreima2  30410  fvdifsupp  30426  cycpmco2f1  30766  cycpmco2lem1  30768  cycpmco2lem5  30772  cycpmco2  30775  cyc3co2  30782  tocyccntz  30786  fedgmullem2  31026  qqhval2  31223  esum2dlem  31351  carsgclctunlem1  31575  sibfof  31598  sitgaddlemb  31606  eulerpartlemsv2  31616  eulerpartlemv  31622  eulerpartlemgs2  31638  dochnel2  38527  nelsubginvcld  39126  nelsubgcld  39127  fltne  39270  rmspecnonsq  39502  disjiun2  41318  dstregt0  41545  fprodexp  41873  fprodabs2  41874  fprodcnlem  41878  lptre2pt  41919  dvnprodlem2  42230  stoweidlem43  42327  fourierdlem66  42456  hsphoidmvle2  42866  hsphoidmvle  42867  hoidmvlelem1  42876  hoidmvlelem2  42877  hoidmvlelem3  42878  hoidmvlelem4  42879  readdcnnred  43502  resubcnnred  43503  recnmulnred  43504  cndivrenred  43505