Theorem eldifbd 3926

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-dif 3916

This theorem is referenced by:  xpdifid  6125  boxcutc  8886  infeq5i  9581  cantnflem2  9635  ackbij1lem18  10182  infpssrlem4  10251  fin23lem30  10287  domtriomlem  10387  pwfseqlem4  10607  dvdsaddre2b  16200  dprdfadd  19813  pgpfac1lem2  19868  pgpfac1lem3a  19869  pgpfac1lem3  19870  lspsolv  20663  lsppratlem3  20669  frlmssuvc2  21238  mplsubrglem  21447  hauscmplem  22794  1stccnp  22850  1stckgen  22942  alexsublem  23432  bcthlem4  24728  plyeq0lem  25608  ftalem3  26461  tglngne  27555  1loopgrvd0  28515  disjiunel  31581  ofpreima2  31649  fvdifsupp  31666  nn0difffzod  31776  cycpmco2f1  32043  cycpmco2lem1  32045  cycpmco2lem5  32049  cycpmco2  32052  cyc3co2  32059  tocyccntz  32063  gsummoncoe1fzo  32367  fedgmullem2  32412  qqhval2  32652  esum2dlem  32780  carsgclctunlem1  33006  sibfof  33029  sitgaddlemb  33037  eulerpartlemsv2  33047  eulerpartlemv  33053  eulerpartlemgs2  33069  dochnel2  39928  nelsubginvcld  40739  nelsubgcld  40740  fltne  41040  rmspecnonsq  41288  disjiun2  43388  dstregt0  43636  fprodexp  43955  fprodabs2  43956  fprodcnlem  43960  lptre2pt  44001  dvnprodlem2  44308  stoweidlem43  44404  fourierdlem66  44533  iundjiunlem  44820  hsphoidmvle2  44946  hsphoidmvle  44947  hoidmvlelem1  44956  hoidmvlelem2  44957  hoidmvlelem3  44958  hoidmvlelem4  44959  readdcnnred  45655  resubcnnred  45656  recnmulnred  45657  cndivrenred  45658