Theorem eqssd 3953

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 3951	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
4	1, 2, 3	sylanbrc 592	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   = wceq 1560   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-ss 3921

This theorem is referenced by:  eqelssd  3957  uneqdifeq  4446  pweq  4569  unieq  4876  unissel  4898  intmin  4926  unissint  4930  int0el  4937  intidg  5424  dmcosseq  5954  dmcosseqOLD  5955  dmcosseqOLDOLD  5956  imadifssran  6136  sofld  6173  relfld  6262  preddowncl  6319  frpoind  6329  tz7.7  6372  f1imadifssran  6607  knatar  7341  sorpssuni  7715  sorpssint  7716  onint  7773  fo2ndf  8100  suppimacnv  8154  tposeq  8208  frrlem14  8280  onfununi  8312  tfrlem15  8363  oaass  8530  odi  8548  omass  8549  oelim2  8565  oeeui  8572  nnawordex  8607  oaabslem  8617  oaabs2  8619  omabslem  8620  omabs  8621  cofon1  8642  uniinqs  8779  sucdom2  9171  onomeneq  9182  fineqv  9211  dffi2  9369  fiuni  9374  dffi3  9377  hartogslem1  9490  ixpiunwdom  9538  cantnfp1lem3  9635  oemapvali  9639  cantnf  9648  dfttrcl2  9679  frind  9708  r1val1  9744  rankval3b  9784  rankunb  9808  rankuni2b  9811  rankr1id  9820  rankc2  9829  rankxplim  9837  tcrank  9842  carden2b  9925  harval2  9955  en2other2  9965  infpwfien  10018  coflim  10218  cfcof  10231  cfidm  10232  isf32lem2  10311  fin1a2lem11  10367  fin1a2lem13  10369  ttukeylem7  10472  fpwwe2  10601  winafp  10655  wuncidm  10704  wuncval2  10705  tskuni  10741  grur1  10778  distrpr  10986  ltexpri  11001  reclem4pr  11008  fzopth  13566  fzosplit  13698  fzouzsplit  13700  fzoopth  13768  ccatrn  14603  cotrtrclfv  15025  dmtrclfv  15031  dfrtrcl2  15075  structcnvcnv  17189  imasaddfnlem  17558  imasvscafn  17567  mrcuni  17653  mressmrcd  17659  submrc  17660  ssceq  17859  rescabs  17866  setcepi  18121  clatl  18540  ipopos  18568  psdmrn  18605  dirdm  18632  gsumress  18716  gsumvallem2  18868  gsumwspan  18880  trivsubgd  19194  trivsubgsnd  19195  trivnsgd  19213  cycsubg  19249  kerf1ghm  19287  conjnmz  19292  pmtrprfv  19493  symggen  19510  odf1o2  19613  gex1  19631  sylow2alem1  19657  smndlsmidm  19696  lsmss1  19705  lsmss2  19707  lsmmod  19715  lsmdisj  19721  lsmdisj2  19722  cntzcmn  19880  prmcyg  19934  dmdprdd  20041  dprdspan  20069  dprdres  20070  dprdz  20072  subgdmdprd  20076  subgdprd  20077  dprddisj2  20081  dprd2dlem1  20083  dprd2da  20084  dmdprdsplit2lem  20087  dprdsplit  20090  ablfacrp  20108  pgpfac1lem3  20119  issubdrg  20829  lspun  21054  lspsn  21069  lspsnneg  21073  lsp0  21076  lsslsp  21082  lmhmlsp  21116  lspextmo  21123  lsmsp  21153  lspprabs  21162  lspsnvs  21184  lspdisj  21195  lsmcv  21211  lspsnat  21215  lsppratlem6  21222  lspprat  21223  lbsextlem4  21231  lidl1el  21296  drngnidl  21313  lidldvgen  21404  cnsubrg  21479  mulgrhm2  21530  znrrg  21617  ocvin  21726  ocvlsp  21728  mrccss  21746  topsn  22991  eltg4i  23020  unitg  23027  tgtop  23033  tgidm  23040  en2top  23045  basgen  23048  2basgen  23050  fctop  23064  cctop  23066  ppttop  23067  epttop  23069  ntrin  23121  isopn3  23126  opnnei  23180  neiuni  23182  maxlp  23207  clslp  23208  tgrest  23219  resttopon  23221  rest0  23229  restcls  23241  restntr  23242  ordtbas2  23251  ordtbas  23252  ordtrest2  23264  cmpcov2  23450  tgcmp  23461  cmpcld  23462  uncmp  23463  cmpfi  23468  dis2ndc  23520  restnlly  23542  dislly  23557  comppfsc  23592  kgentopon  23598  kgencmp  23605  kgenidm  23607  iskgen2  23608  kgencn3  23618  ptuni2  23636  ptbasfi  23641  xkouni  23659  txcls  23664  txdis  23692  txindis  23694  txcmplem2  23702  xkopt  23715  txconn  23749  qtopval2  23756  qtopuni  23762  qtoprest  23777  qtopomap  23778  qtopcmap  23779  kqsat  23791  kqcldsat  23793  hmeocls  23828  hmeontr  23829  hmphdis  23856  fgfil  23935  fgabs  23939  trfil1  23946  fgtr  23950  uzrest  23957  ufilmax  23967  ufileu  23979  filufint  23980  ufildom1  23986  rnelfm  24013  flimfil  24029  uffclsflim  24091  alexsublem  24104  alexsubALTlem3  24109  alexsubALT  24111  ptcmplem2  24113  ptcmplem3  24114  tgpconncompeqg  24172  haustsms2  24197  tgptsmscls  24210  ust0  24280  ustbas2  24285  iccntr  24882  pi1xfrcnv  25119  clsocv  25312  cfilfcls  25336  equivcmet  25379  hlhil  25505  evthicc2  25522  ovolshft  25573  volsup  25618  dyadmbllem  25661  mbfconstlem  25689  itg11  25753  limciun  25956  dvnres  25993  cpnord  25997  dvcmulf  26007  dvmptcmul  26026  dvcnvre  26081  plyco0  26252  taylthlem1  26436  taylthlem2  26437  ulmdvlem3  26465  wilthlem2  27133  ppisval  27168  ppinprm  27216  chtnprm  27218  ltsval2  27720  noextenddif  27732  cutsun12  27883  madebdaylemlrcut  27992  bdayiun  28008  cofcut1  28013  negbday  28150  oniso  28364  bdayons  28369  addonbday  28372  bdayn0p1  28462  plngrot  28997  upgrex  29293  uvtxnbgr  29601  cusgredg  29625  ubthlem1  31073  pjhth  31596  ococin  31611  chsupsn  31616  ssjo  31650  chabs1  31719  spansncvi  31855  mdslj1i  32522  mdslj2i  32523  atomli  32585  atcvatlem  32588  atcvat3i  32599  sumdmdlem  32621  difininv  32716  fnpreimac  32872  pmtrcnelor  33271  cycpmrn  33323  elrgspnlem4  33426  isdrng4  33482  fldgenid  33506  1fldgenq  33509  rspidlid  33561  0ringidl  33607  drngmxidl  33665  drngmxidlr  33666  esplyfvaln  33871  resssra  33884  dimkerim  33924  fldextrspunlem1  33972  fldextrspunlem2  33974  algextdeglem4  34017  cmpcref  34147  zarcls1  34166  zarclssn  34170  zart0  34176  zarcmplem  34178  xpinpreima2  34204  ordtrest2NEW  34220  sigagenid  34448  imambfm  34559  reprinfz1  34916  bnj1136  35292  bnj1398  35329  bnj1408  35331  bnj1498  35356  rankval4b  35396  r1omhfb  35408  fineqvacALT  35413  r1omhfbregs  35433  vonf1oonfo  35458  sconnpi1  35589  cvmliftlem15  35648  altopthsn  36311  opnbnd  36685  opnregcld  36690  cldregopn  36691  fnessref  36717  neibastop1  36719  topmeet  36724  topjoin  36725  fnemeet1  36726  fnejoin1  36728  ttctrid  36862  dfttc2g  36866  dfttc3gw  36883  bj-gabeqd  37422  bj-restpw  37582  bj-restb  37584  bj-restuni2  37588  dissneqlem  37834  pibt2  37911  lindsenlbs  38114  poimirlem13  38132  poimirlem14  38133  poimirlem15  38134  fdc  38244  sstotbnd2  38273  isbnd2  38282  totbndbnd  38288  prdstotbnd  38293  heibor1  38309  1idl  38525  igenval2  38565  idreseqidinxp  38814  disjdmqs  39406  lshpdisj  39611  lssats  39636  lsatcvat3  39676  lshpset2N  39743  lfl1dim  39745  lfl1dim2N  39746  lkrpssN  39787  paddass  40462  paddidm  40465  pmod1i  40472  pmapjat1  40477  pclbtwnN  40521  pclunN  40522  paddunN  40551  pclfinclN  40574  dihjust  41841  dihmeetlem1N  41914  dihglblem5apreN  41915  dihmeetlem13N  41943  dochocsp  42003  dochdmj1  42014  dochnoncon  42015  dihjatb  42040  dihjat1lem  42052  lcfl9a  42129  lclkrlem2s  42149  lclkrlem2v  42152  mapdrvallem3  42270  mapdunirnN  42274  mapdin  42286  mapdlsm  42288  baerlem3lem2  42334  baerlem5alem2  42335  baerlem5blem2  42336  hdmaplkr  42537  primrootsunit1  42714  sticksstones11  42773  aks6d1c6lem5  42794  unitscyglem4  42815  rntrclfvOAI  43272  ismrcd1  43279  ismrcd2  43280  isnacs3  43291  nacsfix  43293  rgspnid  43745  iocinico  43789  onsupmaxb  43816  onsssupeqcond  43857  oacl2g  43907  omabs2  43909  omcl2  43910  ofoaf  43932  onsucunifi  43947  naddwordnexlem4  43978  harval3  44114  mptrcllem  44189  clcnvlem  44199  dmtrcl  44203  rntrcl  44204  cbviuneq12df  44237  dfrcl2  44250  dftrcl3  44296  brtrclfv2  44303  dfrtrcl3  44309  scottrankd  44824  nzin  44894  iunincfi  45672  founiiun  45757  founiiun0  45768  inmap  45785  difmapsn  45788  funimaeq  45821  iuneqfzuz  45911  supminfrnmpt  46019  supminfxr2  46043  supminfxrrnmpt  46045  pimxrneun  46062  iooiinicc  46118  icomnfinre  46128  iooiinioc  46132  limsupresxr  46340  liminfresxr  46341  limsup10exlem  46346  liminfvalxr  46357  fourierdlem79  46759  rrxsnicc  46874  prsal  46892  issalgend  46912  sge0f1o  46956  caragenuni  47085  caragendifcl  47088  opnvonmbllem2  47207  iinhoiicc  47248  pimconstlt1  47276  pimltpnff  47277  pimiooltgt  47284  pimgtmnf2  47288  pimdecfgtioc  47289  pimincfltioc  47290  pimdecfgtioo  47291  pimincfltioo  47292  preimageiingt  47294  preimaleiinlt  47295  pimgtmnff  47296  sssmf  47312  smflimlem5  47349  smfmullem4  47368  smfpimbor1lem2  47373  smfsuplem1  47385  smfpimne2  47414  fsupdm  47416  finfdm  47420  sprsymrelf1  48102  lspeqlco  49061  iunlub  49442  iinglb  49443  iuneqconst2  49444  iineqconst2  49445  isclatd  49604  intubeu  49605  unilbeu  49606  setrecsres  50323