Theorem eqssd 3929

Description: Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 27-Jun-2004.)

Hypotheses

Ref	Expression
eqssd.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
eqssd.2	⊢ (𝜑 → 𝐵 ⊆ 𝐴)

Assertion

Ref	Expression
eqssd	⊢ (𝜑 → 𝐴 = 𝐵)

Proof of Theorem eqssd

Step	Hyp	Ref	Expression
1		eqssd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		eqssd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
3		eqss 3927	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
4	1, 2, 3	sylanbrc 595	1 ⊢ (𝜑 → 𝐴 = 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3899

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 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-ss 3900

This theorem is used by:  eqelssd  3933  uneqdifeq  4450  pweq  4573  unieq  4880  unissel  4902  intmin  4930  unissint  4934  int0el  4941  intidg  5428  dmcosseq  5964  dmcosseqOLD  5965  sofld  6184  imadifssranOLD  6208  imadifssranOLDOLD  6209  relfld  6283  preddowncl  6341  frpoind  6351  tz7.7  6394  knatar  7374  sorpssuni  7755  sorpssint  7756  onint  7811  fo2ndf  8142  suppimacnv  8202  tposeq  8256  frrlem14  8328  onfununi  8360  tfrlem15  8411  oaass  8580  odi  8598  omass  8599  oelim2  8615  oeeui  8622  nnawordex  8657  oaabslem  8667  oaabs2  8669  omabslem  8670  omabs  8671  cofon1  8692  uniinqs  8829  sucdom2  9229  onomeneq  9240  fineqv  9269  dffi2  9425  fiuni  9430  dffi3  9433  hartogslem1  9546  ixpiunwdom  9594  cantnfp1lem3  9691  oemapvali  9695  cantnf  9704  dfttrcl2  9735  frind  9764  r1val1  9803  rankval3b  9846  rankunb  9874  rankuni2b  9877  rankr1id  9888  rankval4b  9890  rankc2  9898  rankxplim  9906  tcrank  9911  scottrankd  9959  carden2b  10058  harval2  10088  en2other2  10098  infpwfien  10151  coflim  10349  cfcof  10362  cfidm  10363  isf32lem2  10442  fin1a2lem11  10498  fin1a2lem13  10500  ttukeylem7  10603  fpwwe2  10738  winafp  10792  wuncidm  10841  wuncval2  10842  tskuni  10878  grur1  10915  distrpr  11123  ltexpri  11138  reclem4pr  11145  fzopth  13705  fzosplit  13837  fzouzsplit  13839  fzoopth  13907  ccatrn  14745  cotrtrclfv  15177  dmtrclfv  15183  dfrtrcl2  15227  structcnvcnv  17343  imasaddfnlem  17712  imasvscafn  17721  mrcuni  17807  mressmrcd  17813  submrc  17814  ssceq  18013  rescabs  18020  setcepi  18275  clatl  18694  ipopos  18722  psdmrn  18759  dirdm  18786  gsumress  18883  gsumvallem2  19042  gsumwspan  19054  trivsubgd  19375  trivsubgsnd  19376  trivnsgd  19394  cycsubg  19435  kerf1ghm  19473  conjnmz  19478  pmtrprfv  19679  symggen  19696  odf1o2  19799  gex1  19817  sylow2alem1  19843  smndlsmidm  19882  lsmss1  19891  lsmss2  19893  lsmmod  19901  lsmdisj  19907  lsmdisj2  19908  cntzcmn  20066  prmcyg  20120  dmdprdd  20227  dprdspan  20255  dprdres  20256  dprdz  20258  subgdmdprd  20262  subgdprd  20263  dprddisj2  20267  dprd2dlem1  20269  dprd2da  20270  dmdprdsplit2lem  20273  dprdsplit  20276  ablfacrp  20294  pgpfac1lem3  20305  isdrng4  21004  issubdrg  21049  lspun  21274  lspsn  21289  lspsnneg  21293  lsp0  21296  lsslsp  21302  lmhmlsp  21336  lspextmo  21343  lsmsp  21373  lspprabs  21382  lspsnvs  21404  lspdisj  21415  lsmcv  21431  lspsnat  21435  lsppratlem6  21442  lspprat  21443  lbsextlem4  21451  lidl1el  21517  0ringidl  21526  rspprop  21536  drngnidl  21543  lidldvgen  21670  cnsubrg  21745  mulgrhm2  21796  znrrg  21883  ocvin  21992  ocvlsp  21994  mrccss  22012  lindsenlbs  22169  topsn  23261  eltg4i  23290  unitg  23297  tgtop  23303  tgidm  23310  en2top  23315  basgen  23318  2basgen  23320  fctop  23334  cctop  23336  ppttop  23337  epttop  23339  ntrin  23391  isopn3  23396  opnnei  23450  neiuni  23452  maxlp  23477  clslp  23478  tgrest  23489  resttopon  23491  rest0  23499  restcls  23511  restntr  23512  ordtbas2  23521  ordtbas  23522  ordtrest2  23534  cmpcov2  23720  tgcmp  23731  cmpcld  23732  uncmp  23733  cmpfi  23738  dis2ndc  23791  restnlly  23813  dislly  23828  comppfsc  23863  kgentopon  23869  kgencmp  23876  kgenidm  23878  iskgen2  23879  kgencn3  23889  ptuni2  23907  ptbasfi  23912  xkouni  23930  txcls  23935  txdis  23963  txindis  23965  txcmplem2  23973  xkopt  23986  txconn  24020  qtopval2  24027  qtopuni  24033  qtoprest  24048  qtopomap  24049  qtopcmap  24050  kqsat  24062  kqcldsat  24064  hmeocls  24099  hmeontr  24100  hmphdis  24127  fgfil  24206  fgabs  24210  trfil1  24217  fgtr  24221  uzrest  24228  ufilmax  24238  ufileu  24250  filufint  24251  ufildom1  24257  rnelfm  24284  flimfil  24300  uffclsflim  24362  alexsublem  24375  alexsubALTlem3  24380  alexsubALT  24382  ptcmplem2  24384  ptcmplem3  24385  tgpconncompeqg  24443  haustsms2  24468  tgptsmscls  24481  ust0  24551  ustbas2  24556  iccntr  25153  pi1xfrcnv  25390  clsocv  25583  cfilfcls  25607  equivcmet  25650  hlhil  25776  evthicc2  25793  ovolshft  25844  volsup  25889  dyadmbllem  25932  mbfconstlem  25960  itg11  26024  limciun  26226  dvnres  26263  cpnord  26267  dvcmulf  26277  dvmptcmul  26296  dvcnvre  26351  plyco0  26522  taylthlem1  26712  taylthlem2  26713  ulmdvlem3  26741  wilthlem2  27408  ppisval  27443  ppinprm  27491  chtnprm  27493  ltsval2  28025  noextenddif  28037  cutsun12  28188  madebdaylemlrcut  28297  bdayiun  28313  cofcut1  28318  negbday  28455  oniso  28669  bdayons  28674  addonbday  28677  bdayn0p1  28767  plngrot  29280  upgrex  29682  uvtxnbgr  29993  cusgredg  30017  ubthlem1  31484  pjhth  32007  ococin  32022  chsupsn  32027  ssjo  32061  chabs1  32130  spansncvi  32266  mdslj1i  32933  mdslj2i  32934  atomli  32996  atcvatlem  32999  atcvat3i  33010  sumdmdlem  33032  difininv  33167  fnpreimac  33318  pmtrcnelor  33705  cycpmrn  33757  elrgspnlem4  33859  fldgenid  33934  1fldgenq  33937  rspidlid  33983  drngmxidl  34054  drngmxidlr  34055  esplyfvaln  34259  resssra  34272  dimkerim  34312  fldextrspunlem1  34360  fldextrspunlem2  34362  algextdeglem4  34405  cmpcref  34535  zarcls1  34554  zarclssn  34558  zart0  34564  zarcmplem  34566  xpinpreima2  34592  ordtrest2NEW  34608  sigagenid  34837  imambfm  34947  reprinfz1  35304  bnj1136  35680  bnj1398  35717  bnj1408  35719  bnj1498  35744  r1omhfb  35799  elscottrankeq  35809  fineqvacALT  35856  r1omhfbregs  35876  vonf1oonfo  36003  sconnpi1  36125  cvmliftlem15  36184  altopthsn  36853  nadddi  37100  opnbnd  37240  opnregcld  37245  cldregopn  37246  fnessref  37272  neibastop1  37274  topmeet  37279  topjoin  37280  fnemeet1  37281  fnejoin1  37283  ttctrid  37417  dfttc2g  37421  dfttc3gw  37438  bj-gabeqd  37977  bj-restpw  38152  bj-restb  38154  bj-restuni2  38158  dissneqlem  38403  pibt2  38480  poimirlem13  38691  poimirlem14  38692  poimirlem15  38693  fdc  38819  sstotbnd2  38848  isbnd2  38857  totbndbnd  38863  prdstotbnd  38868  heibor1  38884  1idl  39100  igenval2  39140  idreseqidinxp  39387  disjdmqs  39979  lshpdisj  40184  lssats  40209  lsatcvat3  40249  lshpset2N  40316  lfl1dim  40318  lfl1dim2N  40319  lkrpssN  40360  paddass  41035  paddidm  41038  pmod1i  41045  pmapjat1  41050  pclbtwnN  41094  pclunN  41095  paddunN  41124  pclfinclN  41147  dihjust  42414  dihmeetlem1N  42487  dihglblem5apreN  42488  dihmeetlem13N  42516  dochocsp  42576  dochdmj1  42587  dochnoncon  42588  dihjatb  42613  dihjat1lem  42625  lcfl9a  42702  lclkrlem2s  42722  lclkrlem2v  42725  mapdrvallem3  42843  mapdunirnN  42847  mapdin  42859  mapdlsm  42861  baerlem3lem2  42907  baerlem5alem2  42908  baerlem5blem2  42909  hdmaplkr  43110  primrootsunit1  43287  sticksstones11  43346  aks6d1c6lem5  43367  unitscyglem4  43388  rntrclfvOAI  43842  ismrcd1  43849  ismrcd2  43850  isnacs3  43861  nacsfix  43863  rgspnid  44310  iocinico  44354  onsupmaxb  44381  onsssupeqcond  44422  oacl2g  44472  omabs2  44474  omcl2  44475  ofoaf  44497  onsucunifi  44512  naddwordnexlem4  44543  harval3  44679  mptrcllem  44753  clcnvlem  44763  dmtrcl  44767  rntrcl  44768  cbviuneq12df  44801  dfrcl2  44814  dftrcl3  44860  brtrclfv2  44867  dfrtrcl3  44873  nzin  45442  iunincfi  46248  founiiun  46333  founiiun0  46344  inmap  46361  difmapsn  46364  funimaeq  46397  iuneqfzuz  46486  supminfrnmpt  46594  supminfxr2  46618  supminfxrrnmpt  46620  pimxrneun  46637  iooiinicc  46693  icomnfinre  46703  iooiinioc  46707  limsupresxr  46915  liminfresxr  46916  limsup10exlem  46921  liminfvalxr  46932  fourierdlem79  47334  rrxsnicc  47449  prsal  47467  issalgend  47487  sge0f1o  47531  caragenuni  47660  caragendifcl  47663  opnvonmbllem2  47782  iinhoiicc  47823  pimconstlt1  47851  pimltpnff  47852  pimiooltgt  47859  pimgtmnf2  47863  pimdecfgtioc  47864  pimincfltioc  47865  pimdecfgtioo  47866  pimincfltioo  47867  preimageiingt  47869  preimaleiinlt  47870  pimgtmnff  47871  sssmf  47887  smflimlem5  47924  smfmullem4  47943  smfpimbor1lem2  47948  smfsuplem1  47960  smfpimne2  47989  fsupdm  47991  finfdm  47995  tmachlem-agreesn  48096  sprsymrelf1  48717  lspeqlco  49690  iunlub  50071  iinglb  50072  iuneqconst2  50073  iineqconst2  50074  isclatd  50236  intubeu  50237  unilbeu  50238  setrecsres  51009