Theorem eldifad 3176

Description: If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3174. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
eldifad.1	⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))

Assertion

Ref	Expression
eldifad	⊢ (𝜑 → 𝐴 ∈ 𝐵)

Proof of Theorem eldifad

Step	Hyp	Ref	Expression
1		eldifad.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))
2		eldif 3174	. . 3 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
3	1, 2	sylib 122	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
4	3	simpld 112	1 ⊢ (𝜑 → 𝐴 ∈ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∈ wcel 2175   ∖ cdif 3162

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-dif 3167

This theorem is referenced by:  fimax2gtri  6997  finexdc  6998  unfidisj  7018  undifdc  7020  ssfirab  7032  fnfi  7037  iunfidisj  7047  dcfi  7082  hashunlem  10947  zfz1isolemiso  10982  fsumrelem  11753  fprodcl2lem  11887  fprodap0  11903  fprodrec  11911  fprodap0f  11918  fprodle  11922  iuncld  14558  fsumcncntop  15010  gausslemma2dlem0i  15505  gausslemma2dlem4  15512  gausslemma2dlem5a  15513  gausslemma2dlem7  15516  lgseisenlem1  15518  lgseisenlem2  15519  lgseisenlem3  15520  lgseisenlem4  15521  lgseisen  15522  lgsquadlem1  15525  lgsquadlem2  15526  lgsquadlem3  15527  bj-charfun  15705