Theorem difss 4098

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 4093	. 2 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐴)
2	1	ssriv 3949	1 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴

Syntax hints:   ∖ cdif 3910   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-ss 3930

This theorem is referenced by:  difssd  4099  difss2  4100  ssdifss  4102  0dif  4368  disj4  4422  difsnpss  4776  unidif  4909  iunxdif2  5019  difexg  5297  difelpw  5322  reldif  5800  cnvdif  6138  difxp  6160  frpoind  6340  tz7.7  6383  fresaun  6747  fresaunres2  6748  resdif  6840  fndmdif  7035  tfi  7845  peano5  7886  oelim2  8577  swoer  8722  swoord1  8723  swoord2  8724  ralxpmap  8890  boxcutc  8935  undom  9049  domunsncan  9061  sbthlem2  9072  sbthlem4  9074  sbthlem5  9075  limenpsi  9136  diffi  9155  php3  9189  frfi  9241  fofinf1o  9285  ixpfi2  9303  elfiun  9386  marypha1lem  9389  wemapso  9509  infdifsn  9622  cantnflem2  9655  frind  9718  frr1  9727  dfac8alem  10009  acnnum  10032  inffien  10043  kmlem5  10134  infdif  10187  infdif2  10188  ackbij1lem18  10215  fictb  10223  fin23lem7  10296  fin23lem11  10297  fin23lem28  10320  fin23lem30  10322  compsscnvlem  10350  isf34lem2  10353  compssiso  10354  isf34lem4  10357  fin1a2lem7  10386  axcclem  10437  zornn0g  10485  ttukey2g  10496  pinn  10859  niex  10862  ltsopi  10869  dmaddpi  10871  dmmulpi  10872  lerelxr  11268  mulnzcnf  11856  dflt2  13169  expcl2lem  14105  expclzlem  14115  hashun2  14415  fsumss  15772  fsumless  15844  cvgcmpce  15866  fprodss  15998  rpnnen2lem9  16274  isstruct2  17205  structcnvcnv  17209  strleun  17213  strle1  17214  fsets  17225  mreexexlem2d  17697  gsumpropd2lem  18733  symgfixf1  19503  f1omvdmvd  19509  mvdco  19511  f1omvdconj  19512  pmtrfb  19531  pmtrfconj  19532  symggen  19536  symggen2  19537  psgnunilem1  19559  frgpnabllem2  19940  dprdss  20097  dprd2da  20110  dmdprdsplit2lem  20113  dpjidcl  20126  ablfac1b  20138  ablfac1eu  20141  isdomn3  20795  isdrng2  20823  drngid2  20831  isdrngd  20843  isdrngdOLD  20845  cntzsdrg  20879  subdrgint  20880  prmidlsubm  21452  cnmgpid  21544  cnmsubglem  21545  xrs1mnd  21555  xrs10  21556  xrs1cmn  21557  xrge0subm  21558  xrge0cmn  21559  expghm  21590  dsmmfi  21853  islinds2  21928  lindsind2  21934  lindfrn  21936  islindf4  21953  psdmul  22294  mdetdiaglem  22720  mdetrsca2  22726  mdetrlin2  22729  mdetralt  22730  mdetunilem5  22738  mdetunilem9  22742  maducoeval2  22762  smadiadetglem1  22793  isopn2  23154  ntrval2  23173  ntrdif  23174  clsdif  23175  ntrss  23177  cmclsopn  23184  discld  23211  mretopd  23214  lpsscls  23263  restntr  23304  cmpcld  23524  2ndcsep  23581  1stccnp  23584  llycmpkgen2  23672  1stckgen  23676  txkgen  23774  qtopcld  23835  qtopcmap  23841  kqdisj  23854  isufil2  24030  ufileu  24041  filufint  24042  fixufil  24044  cfinufil  24050  ufilen  24052  fin1aufil  24054  supnfcls  24142  flimfnfcls  24150  alexsublem  24166  alexsubALTlem3  24171  cldsubg  24233  imasdsf1olem  24495  recld2  24937  sszcld  24940  xrge0gsumle  24956  divcn  24992  cdivcncf  25045  bcth3  25455  ismbl2  25651  cmmbl  25658  nulmbl  25659  nulmbl2  25660  unmbl  25661  voliunlem1  25674  voliunlem2  25675  ioombl1lem4  25685  ioombl1  25686  uniioombllem3  25709  mbfss  25770  itg1cl  25809  itg1ge0  25810  i1f0  25811  i1f1  25814  i1fmul  25820  itg1addlem4  25823  itg1mulc  25828  itg10a  25834  itg1ge0a  25835  itg1climres  25838  itg2cnlem1  25885  itgioo  25940  itgsplitioo  25962  limcdif  26000  ellimc2  26001  ellimc3  26003  limcflflem  26004  limcflf  26005  limcmo  26006  limcresi  26009  dvreslem  26033  dvres2lem  26034  dvidlem  26039  dvcnp2  26044  dvaddbr  26062  dvmulbr  26063  dvcobr  26070  dvrec  26079  dvcnvlem  26100  lhop1lem  26137  lhop  26140  tdeglem4  26182  deg1n0ima  26211  aacjcl  26453  taylthlem2  26499  abelth  26566  logcnlem5  26773  dvlog2  26780  efopnlem2  26784  dvcncxp1  26870  dvcnsqrt  26871  cxpcn2  26873  sqrtcn  26877  efrlim  27096  jensen  27115  amgm  27117  lgamgulmlem2  27156  lgamucov  27164  wilthlem2  27195  dchrelbas2  27363  rpvmasum2  27638  dchrisum0re  27639  dchrisum0lem3  27645  dchrisum0  27646  nnssn0s  28476  tgisline  28858  upgrss  29375  frgrwopreg2  30607  difxp1ss  32805  difxp2ss  32806  xrge00  33271  symgcom2  33341  pmtrcnel  33346  pmtrcnel2  33347  pmtrcnelor  33348  cycpmrn  33400  tocyccntz  33401  evlextv  33873  vietalem  33910  submatres  34137  madjusmdetlem2  34159  madjusmdetlem3  34160  qtophaus  34167  fsumcvg4  34281  gsumesum  34390  pwsiga  34461  sigainb  34467  carsggect  34649  omsmeas  34654  sitgclg  34673  ballotlemfelz  34822  ballotlemfp1  34823  ballotth  34869  cxpcncf1  34923  logdivsqrle  34978  hgt750lemb  34984  fineqvnttrclse  35456  kur14lem6  35598  kur14lem7  35599  cvmscld  35660  satfvsucsuc  35752  satfrnmapom  35757  mclsppslem  35970  fundmpss  36154  relsset  36273  limitssson  36296  fnsingle  36304  funimage  36313  cldbnd  36722  clsun  36724  topdifinffinlem  37876  inunissunidif  37904  pibt2  37946  matunitlindflem1  38150  poimirlem8  38162  poimirlem26  38180  poimirlem30  38184  mblfinlem3  38193  mblfinlem4  38194  ismblfin  38195  voliunnfl  38198  cnambfre  38202  dvtan  38204  dvasin  38238  dvacos  38239  areacirclem4  38245  fdc  38279  divrngcl  38491  isdrngo2  38492  isdrngo3  38493  islsati  39653  hdmap14lem2a  42526  redvmptabs  43004  prjspreln0  43226  prjspvs  43227  prjspeclsp  43229  0prjspnrel  43244  istopclsd  43316  diophin  43388  dnnumch1  43656  deg1mhm  43812  gneispace  44745  inaex  44892  sumnnodd  46231  cncficcgt0  46487  cncfiooicclem1  46492  cxpcncf2  46498  dirkercncflem2  46703  fourierdlem62  46767  fourierdlem66  46771  fourierdlem68  46773  fourierdlem95  46800  etransclem24  46857  etransclem44  46877  gsumge0cl  46970  sge0fodjrnlem  47015  carageniuncllem1  47120  smfresal  47387  dfnbgrss  48499  dfnbgrss2  48506  lindslinindimp2lem2  49117  iscnrm3rlem2  49597  amgmlemALT  50459