Theorem difss 4073

Description: Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)

Assertion

Ref	Expression
difss	⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴

Proof of Theorem difss

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eldifi 4068	. 2 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐴)
2	1	ssriv 3926	1 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴

Syntax hints:   ∖ cdif 3887   ⊆ wss 3890

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-dif 3893  df-ss 3907

This theorem is referenced by:  difssd  4074  difss2  4075  ssdifss  4077  0dif  4340  disj4  4394  difsnpss  4747  unidif  4880  iunxdif2  4990  difexg  5264  difelpw  5289  reldif  5765  cnvdif  6101  difxp  6122  frpoind  6300  tz7.7  6343  fresaun  6705  fresaunres2  6706  resdif  6795  fndmdif  6990  tfi  7800  peano5  7840  oelim2  8528  swoer  8672  swoord1  8673  swoord2  8674  ralxpmap  8841  boxcutc  8886  undom  9000  domunsncan  9012  sbthlem2  9023  sbthlem4  9025  sbthlem5  9026  limenpsi  9087  diffi  9106  php3  9140  frfi  9192  fofinf1o  9239  ixpfi2  9257  elfiun  9340  marypha1lem  9343  wemapso  9463  infdifsn  9576  cantnflem2  9609  frind  9672  frr1  9681  dfac8alem  9949  acnnum  9972  inffien  9983  kmlem5  10075  infdif  10128  infdif2  10129  ackbij1lem18  10156  fictb  10164  fin23lem7  10236  fin23lem11  10237  fin23lem28  10260  fin23lem30  10262  compsscnvlem  10290  isf34lem2  10293  compssiso  10294  isf34lem4  10297  fin1a2lem7  10326  axcclem  10377  zornn0g  10425  ttukey2g  10436  pinn  10799  niex  10802  ltsopi  10809  dmaddpi  10811  dmmulpi  10812  lerelxr  11206  mulnzcnf  11794  dflt2  13097  expcl2lem  14033  expclzlem  14043  hashun2  14343  fsumss  15685  fsumless  15757  cvgcmpce  15779  fprodss  15911  rpnnen2lem9  16187  isstruct2  17117  structcnvcnv  17121  strleun  17125  strle1  17126  fsets  17137  mreexexlem2d  17609  gsumpropd2lem  18645  symgfixf1  19410  f1omvdmvd  19416  mvdco  19418  f1omvdconj  19419  pmtrfb  19438  pmtrfconj  19439  symggen  19443  symggen2  19444  psgnunilem1  19466  frgpnabllem2  19847  dprdss  20004  dprd2da  20017  dmdprdsplit2lem  20020  dpjidcl  20033  ablfac1b  20045  ablfac1eu  20048  isdomn3  20694  isdrng2  20722  drngmclOLD  20730  drngid2  20731  isdrngd  20744  isdrngdOLD  20746  cntzsdrg  20781  subdrgint  20782  cnmgpid  21411  cnmsubglem  21412  xrs1mnd  21422  xrs10  21423  xrs1cmn  21424  xrge0subm  21425  xrge0cmn  21426  expghm  21457  dsmmfi  21720  islinds2  21795  lindsind2  21801  lindfrn  21803  islindf4  21820  psdmul  22161  mdetdiaglem  22588  mdetrsca2  22594  mdetrlin2  22597  mdetralt  22598  mdetunilem5  22606  mdetunilem9  22610  maducoeval2  22630  smadiadetglem1  22661  isopn2  23022  ntrval2  23041  ntrdif  23042  clsdif  23043  ntrss  23045  cmclsopn  23052  discld  23079  mretopd  23082  lpsscls  23131  restntr  23172  cmpcld  23392  2ndcsep  23449  1stccnp  23452  llycmpkgen2  23540  1stckgen  23544  txkgen  23642  qtopcld  23703  qtopcmap  23709  kqdisj  23722  isufil2  23898  ufileu  23909  filufint  23910  fixufil  23912  cfinufil  23918  ufilen  23920  fin1aufil  23922  supnfcls  24010  flimfnfcls  24018  alexsublem  24034  alexsubALTlem3  24039  cldsubg  24101  imasdsf1olem  24363  recld2  24805  sszcld  24808  xrge0gsumle  24824  divcn  24860  cdivcncf  24913  bcth3  25323  ismbl2  25519  cmmbl  25526  nulmbl  25527  nulmbl2  25528  unmbl  25529  voliunlem1  25542  voliunlem2  25543  ioombl1lem4  25553  ioombl1  25554  uniioombllem3  25577  mbfss  25638  itg1cl  25677  itg1ge0  25678  i1f0  25679  i1f1  25682  i1fmul  25688  itg1addlem4  25691  itg1mulc  25696  itg10a  25702  itg1ge0a  25703  itg1climres  25706  itg2cnlem1  25753  itgioo  25808  itgsplitioo  25830  limcdif  25868  ellimc2  25869  ellimc3  25871  limcflflem  25872  limcflf  25873  limcmo  25874  limcresi  25877  dvreslem  25901  dvres2lem  25902  dvidlem  25907  dvcnp2  25912  dvaddbr  25930  dvmulbr  25931  dvcobr  25938  dvrec  25947  dvcnvlem  25968  lhop1lem  26005  lhop  26008  tdeglem4  26050  deg1n0ima  26079  aacjcl  26318  taylthlem2  26364  abelth  26431  logcnlem5  26635  dvlog2  26642  efopnlem2  26646  dvcncxp1  26732  dvcnsqrt  26733  cxpcn2  26735  sqrtcn  26739  efrlim  26958  jensen  26977  amgm  26979  lgamgulmlem2  27018  lgamucov  27026  wilthlem2  27057  dchrelbas2  27225  rpvmasum2  27500  dchrisum0re  27501  dchrisum0lem3  27507  dchrisum0  27508  nnssn0s  28338  tgisline  28720  upgrss  29182  frgrwopreg2  30414  difxp1ss  32617  difxp2ss  32618  xrge00  33100  symgcom2  33172  pmtrcnel  33177  pmtrcnel2  33178  pmtrcnelor  33179  cycpmrn  33231  tocyccntz  33232  evlextv  33733  vietalem  33770  submatres  33997  madjusmdetlem2  34019  madjusmdetlem3  34020  qtophaus  34027  fsumcvg4  34141  gsumesum  34250  pwsiga  34321  sigainb  34327  carsggect  34509  omsmeas  34514  sitgclg  34533  ballotlemfelz  34682  ballotlemfp1  34683  ballotth  34729  cxpcncf1  34786  logdivsqrle  34841  hgt750lemb  34847  fineqvnttrclse  35312  kur14lem6  35446  kur14lem7  35447  cvmscld  35508  satfvsucsuc  35600  satfrnmapom  35605  mclsppslem  35818  fundmpss  36002  relsset  36121  limitssson  36144  fnsingle  36152  funimage  36161  cldbnd  36561  clsun  36563  topdifinffinlem  37716  inunissunidif  37744  pibt2  37786  matunitlindflem1  37990  poimirlem8  38002  poimirlem26  38020  poimirlem30  38024  mblfinlem3  38033  mblfinlem4  38034  ismblfin  38035  voliunnfl  38038  cnambfre  38042  dvtan  38044  dvasin  38078  dvacos  38079  areacirclem4  38085  fdc  38119  divrngcl  38331  isdrngo2  38332  isdrngo3  38333  islsati  39493  hdmap14lem2a  42366  redvmptabs  42844  prjspreln0  43066  prjspvs  43067  prjspeclsp  43069  0prjspnrel  43084  istopclsd  43156  diophin  43228  dnnumch1  43496  deg1mhm  43652  gneispace  44585  inaex  44748  sumnnodd  46082  cncficcgt0  46338  cncfiooicclem1  46343  cxpcncf2  46349  dirkercncflem2  46554  fourierdlem62  46618  fourierdlem66  46622  fourierdlem68  46624  fourierdlem95  46651  etransclem24  46708  etransclem44  46728  gsumge0cl  46821  sge0fodjrnlem  46866  carageniuncllem1  46971  smfresal  47238  dfnbgrss  48350  dfnbgrss2  48357  lindslinindimp2lem2  48957  iscnrm3rlem2  49438  amgmlemALT  50300