Theorem eldifn 4068

Description: Implication of membership in a class difference. (Contributed by NM, 3-May-1994.)

Assertion

Ref	Expression
eldifn	⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → ¬ 𝐴 ∈ 𝐶)

Proof of Theorem eldifn

Step	Hyp	Ref	Expression
1		eldif 4049	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
2	1	simprbi 503	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → ¬ 𝐴 ∈ 𝐶)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2144   ∖ cdif 4045

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 4047

This theorem is used by:  elndif  4069  disjel  4409  tz7.7  6388  partfun  6686  funiunfv  7252  tfi  7864  peano5  7905  resf1extb  7946  frrlem11  8314  frrlem12  8315  frrlem14  8317  tz7.48-2  8452  tz7.49  8455  oaf1o  8571  undifixp  8962  domdifsn  9079  isinf  9256  ordtypelem7  9518  unxpwdom2  9582  inf3lem3  9631  infdifsn  9658  cantnfp1lem1  9679  cantnfp1lem3  9681  cantnflem1d  9689  setind  9748  fin23lem30  10420  domtriomlem  10520  axdc3lem4  10531  axdc4lem  10533  axcclem  10535  ttukeylem7  10593  konigthlem  10653  fpwwe2lem12  10727  fpwwe2  10728  indval2  12325  ind0  12330  hashf1lem1  14600  rlimrecl  15747  sumrblem  15877  fsumcvg  15878  summolem2a  15881  fsumss  15891  sumss2  15892  binomlem  15998  isumltss  16017  prodrblem  16096  fprodcvg  16097  prodmolem2a  16101  fprodss  16115  fprodsplit  16133  fprodmodd  16164  sumodd  16558  prmreclem2  17095  prmreclem5  17098  ramub1lem1  17204  chnccat  18800  efgs1b  19950  gsumzsplit  20141  gsum2d  20186  gsum2d2lem  20187  dmdprdsplitlem  20253  pgpfac1lem1  20290  irredrmul  20657  lbsextlem2  21437  lbsextlem4  21439  prmidlc2  21630  cmprmidlmcl  21631  cnsubrg  21733  psrlidm  22269  mplcoe1  22346  mplcoe5  22349  evlslem3  22389  selvvvval  22451  maducoeval2  22955  madugsum  22958  elcls  23391  isclo  23405  ptbasfi  23900  ptopn2  23903  xkopt  23974  kqdisj  24051  fin1aufil  24251  ptcmplem4  24374  opnsubg  24427  tsmssplit  24471  zcld  25133  recld2  25134  reconnlem1  25146  ioombl1lem4  25882  i1fima2sn  26001  itg1val2  26005  i1f0  26008  itg1addlem4  26020  mbfi1flim  26044  itg2splitlem  26069  itg2split  26070  itg2cnlem1  26082  itg2cnlem2  26083  itgss2  26133  itgeqa  26134  itgss3  26135  itgless  26137  ibladdlem  26140  itgaddlem1  26143  iblabslem  26148  itggt0  26164  itgcn  26165  ply1termlem  26521  plypf1  26531  plyaddlem1  26532  plymullem1  26533  coeeulem  26543  coeidlem  26556  coeid3  26559  coefv0  26567  coemulc  26574  dvply1  26605  vieta1lem2  26634  aaliou2  26667  logdmnrp  26969  regamcl  27388  lgam1  27391  gam1  27392  facgam  27393  chpub  27547  chebbnd1lem1  27796  numedglnl  29722  strlem1  32852  cycpmco2  33694  2sqr3minply  34412  sigaclfu2  34753  eulerpartlemb  35000  acwer1prc  35760  fineqvnttrclse  35792  setindregs  35798  mrsubcn  36284  dfon2lem6  36550  lindsadd  38537  ibladdnclem  38595  itgaddnclem1  38597  iblabsnclem  38602  ftc1anclem5  38616  ftc1anclem6  38617  ftc1anclem8  38619  dvasin  38623  dvacos  38624  pridlc2  39007  pridlc3  39008  idomnnzgmulnz  43184  deg1gprod  43191  readvrec2  43413  readvrec  43414  fsuppssind  43622  irrapx1  43835  pellqrex  43886  qirropth  43915  setindtr  44031  kelac1  44065  flcidc  44172  arearect  44217  areaquad  44218  cantnfub  44323  mpct  46215  difmap  46220  difmapsn  46225  iccdificc  46551  fsumsupp0  46590  mccllem  46609  sumnnodd  46642  fprodcncf  46910  stoweidlem34  47044  stoweidlem44  47054  stirlinglem5  47088  fourierdlem62  47178  fouriersw  47241  elaa2lem  47243  etransclem44  47288  sge0iunmptlemfi  47423  sge0fodjrnlem  47426  meadjiunlem  47475  isomenndlem  47540  hsphoidmvle2  47595  hsphoidmvle  47596  hspdifhsp  47626  hspmbllem2  47637  ovnsubadd2lem  47655  ovolval4lem1  47659  preimagelt  47709  preimalegt  47710  tannpoly  47940  tmachlem-tpopen  47951