Theorem eldifbd 3905

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-dif 3895

This theorem is referenced by:  xpdifid  6070  boxcutc  8712  infeq5i  9372  cantnflem2  9426  ackbij1lem18  9994  infpssrlem4  10063  fin23lem30  10099  domtriomlem  10199  pwfseqlem4  10419  dvdsaddre2b  16014  dprdfadd  19621  pgpfac1lem2  19676  pgpfac1lem3a  19677  pgpfac1lem3  19678  lspsolv  20403  lsppratlem3  20409  frlmssuvc2  21000  mplsubrglem  21208  hauscmplem  22555  1stccnp  22611  1stckgen  22703  alexsublem  23193  bcthlem4  24489  plyeq0lem  25369  ftalem3  26222  tglngne  26909  1loopgrvd0  27869  disjiunel  30931  ofpreima2  30999  fvdifsupp  31014  cycpmco2f1  31387  cycpmco2lem1  31389  cycpmco2lem5  31393  cycpmco2  31396  cyc3co2  31403  tocyccntz  31407  fedgmullem2  31707  qqhval2  31928  esum2dlem  32056  carsgclctunlem1  32280  sibfof  32303  sitgaddlemb  32311  eulerpartlemsv2  32321  eulerpartlemv  32327  eulerpartlemgs2  32343  dochnel2  39402  nelsubginvcld  40217  nelsubgcld  40218  fltne  40478  rmspecnonsq  40726  disjiun2  42576  dstregt0  42790  fprodexp  43106  fprodabs2  43107  fprodcnlem  43111  lptre2pt  43152  dvnprodlem2  43459  stoweidlem43  43555  fourierdlem66  43684  iundjiunlem  43968  hsphoidmvle2  44094  hsphoidmvle  44095  hoidmvlelem1  44104  hoidmvlelem2  44105  hoidmvlelem3  44106  hoidmvlelem4  44107  readdcnnred  44764  resubcnnred  44765  recnmulnred  44766  cndivrenred  44767