Theorem eqssd 3874

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

Syntax hints:   → wi 4   = wceq 1507   ⊆ wss 3828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2747

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2756  df-cleq 2768  df-clel 2843  df-in 3835  df-ss 3842

This theorem is referenced by:  eqelssd  3877  uneqdifeq  4319  unissel  4740  intmin  4767  unissint  4771  int0el  4778  dmcosseq  5683  sofld  5882  relfld  5962  preddowncl  6011  wfi  6017  tz7.7  6053  fimacnv  6662  knatar  6931  sorpssuni  7274  sorpssint  7275  onint  7324  fo2ndf  7619  suppimacnv  7641  tposeq  7694  onfununi  7779  tfrlem15  7829  oaass  7984  odi  8002  omass  8003  oelim2  8018  oeeui  8025  nnawordex  8060  oaabslem  8066  oaabs2  8068  omabslem  8069  omabs  8070  uniinqs  8173  sucdom2  8505  fineqv  8524  dffi2  8678  fiuni  8683  dffi3  8686  hartogslem1  8797  ixpiunwdom  8846  cantnfp1lem3  8933  oemapvali  8937  cantnf  8946  r1val1  9005  rankval3b  9045  rankunb  9069  rankuni2b  9072  rankr1id  9081  rankc2  9090  rankxplim  9098  tcrank  9103  carden2b  9186  harval2  9216  en2other2  9225  infpwfien  9278  coflim  9477  cfcof  9490  cfidm  9491  isf32lem2  9570  fin1a2lem11  9626  fin1a2lem13  9628  ttukeylem7  9731  fpwwe2  9859  winafp  9913  wuncidm  9962  wuncval2  9963  tskuni  9999  grur1  10036  distrpr  10244  ltexpri  10259  reclem4pr  10266  fzopth  12757  fzosplit  12882  fzouzsplit  12884  ccatrn  13746  cotrtrclfv  14227  dmtrclfv  14233  dfrtrcl2  14276  structcnvcnv  16347  imasaddfnlem  16651  imasvscafn  16660  mrcuni  16744  mressmrcd  16750  submrc  16751  ssceq  16948  rescabs  16955  setcepi  17200  clatl  17578  ipopos  17622  psdmrn  17669  dirdm  17696  gsumress  17738  gsumvallem2  17834  gsumwspan  17846  cycsubg  18085  conjnmz  18157  pmtrprfv  18336  symggen  18353  odf1o2  18453  gex1  18471  sylow2alem1  18497  lsmidm  18542  lsmss1  18544  lsmss2  18546  lsmmod  18553  lsmdisj  18559  lsmdisj2  18560  cntzcmn  18712  prmcyg  18762  dmdprdd  18865  dprdspan  18893  dprdres  18894  dprdz  18896  subgdmdprd  18900  subgdprd  18901  dprddisj2  18905  dprd2dlem1  18907  dprd2da  18908  dmdprdsplit2lem  18911  dprdsplit  18914  ablfacrp  18932  pgpfac1lem3  18943  kerf1ghm  19214  kerf1hrmOLD  19215  issubdrg  19277  lspun  19475  lspsn  19490  lspsnneg  19494  lsp0  19497  lsslsp  19503  lmhmlsp  19537  lspextmo  19544  lsmsp  19574  lspprabs  19583  lspsnvs  19602  lspdisj  19613  lsmcv  19629  lspsnat  19633  lsppratlem6  19640  lspprat  19641  lbsextlem4  19649  lidl1el  19706  drngnidl  19717  lidldvgen  19743  cnsubrg  20301  mulgrhm2  20342  znrrg  20408  ocvin  20514  ocvlsp  20516  mrccss  20534  topsn  21237  eltg4i  21266  unitg  21273  tgtop  21279  tgidm  21286  en2top  21291  basgen  21294  2basgen  21296  fctop  21310  cctop  21312  ppttop  21313  epttop  21315  ntrin  21367  isopn3  21372  opnnei  21426  neiuni  21428  maxlp  21453  clslp  21454  tgrest  21465  resttopon  21467  rest0  21475  restcls  21487  restntr  21488  ordtbas2  21497  ordtbas  21498  ordtrest2  21510  cmpcov2  21696  tgcmp  21707  cmpcld  21708  uncmp  21709  cmpfi  21714  dis2ndc  21766  restnlly  21788  dislly  21803  comppfsc  21838  kgentopon  21844  kgencmp  21851  kgenidm  21853  iskgen2  21854  kgencn3  21864  ptuni2  21882  ptbasfi  21887  xkouni  21905  txcls  21910  txdis  21938  txindis  21940  txcmplem2  21948  xkopt  21961  txconn  21995  qtopval2  22002  qtopuni  22008  qtoprest  22023  qtopomap  22024  qtopcmap  22025  kqsat  22037  kqcldsat  22039  hmeocls  22074  hmeontr  22075  hmphdis  22102  fgfil  22181  fgabs  22185  trfil1  22192  fgtr  22196  uzrest  22203  ufilmax  22213  ufileu  22225  filufint  22226  ufildom1  22232  rnelfm  22259  flimfil  22275  uffclsflim  22337  alexsublem  22350  alexsubALTlem3  22355  alexsubALT  22357  ptcmplem2  22359  ptcmplem3  22360  tgpconncompeqg  22417  haustsms2  22442  tgptsmscls  22455  ust0  22525  ustbas2  22531  iccntr  23126  pi1xfrcnv  23358  clsocv  23550  cfilfcls  23574  equivcmet  23617  hlhil  23743  evthicc2  23758  ovolshft  23809  volsup  23854  dyadmbllem  23897  mbfconstlem  23925  itg11  23989  limciun  24189  dvnres  24225  cpnord  24229  dvcmulf  24239  dvmptcmul  24258  dvcnvre  24313  plyco0  24479  taylthlem1  24658  taylthlem2  24659  ulmdvlem3  24687  wilthlem2  25342  ppisval  25377  ppinprm  25425  chtnprm  25427  upgrex  26574  uvtxnbgr  26879  cusgredg  26903  ubthlem1  28419  pjhth  28945  ococin  28960  chsupsn  28965  ssjo  28999  chabs1  29068  spansncvi  29204  mdslj1i  29871  mdslj2i  29872  atomli  29934  atcvatlem  29937  atcvat3i  29948  sumdmdlem  29970  difininv  30049  fnpreimac  30172  dimkerim  30643  cmpcref  30749  xpinpreima2  30785  ordtrest2NEW  30801  sigagenid  31046  imambfm  31156  reprinfz1  31532  bnj1136  31905  bnj1398  31942  bnj1408  31944  bnj1498  31969  sconnpi1  32061  cvmliftlem15  32120  dftrpred3g  32563  trpredpo  32565  frpoind  32571  frind  32576  frrlem14  32627  sltval2  32654  noextenddif  32666  scutun12  32762  altopthsn  32913  opnbnd  33164  opnregcld  33169  cldregopn  33170  fnessref  33196  neibastop1  33198  topmeet  33203  topjoin  33204  fnemeet1  33205  fnejoin1  33207  bj-restpw  33858  bj-restb  33860  bj-restuni2  33864  dissneqlem  34028  pibt2  34104  lindsenlbs  34306  poimirlem13  34324  poimirlem14  34325  poimirlem15  34326  fdc  34440  sstotbnd2  34472  isbnd2  34481  totbndbnd  34487  prdstotbnd  34492  heibor1  34508  1idl  34724  igenval2  34764  idreseqidinxp  34989  lshpdisj  35546  lssats  35571  lsatcvat3  35611  lshpset2N  35678  lfl1dim  35680  lfl1dim2N  35681  lkrpssN  35722  paddass  36397  paddidm  36400  pmod1i  36407  pmapjat1  36412  pclbtwnN  36456  pclunN  36457  paddunN  36486  pclfinclN  36509  dihjust  37776  dihmeetlem1N  37849  dihglblem5apreN  37850  dihmeetlem13N  37878  dochocsp  37938  dochdmj1  37949  dochnoncon  37950  dihjatb  37975  dihjat1lem  37987  lcfl9a  38064  lclkrlem2s  38084  lclkrlem2v  38087  mapdrvallem3  38205  mapdunirnN  38209  mapdin  38221  mapdlsm  38223  baerlem3lem2  38269  baerlem5alem2  38270  baerlem5blem2  38271  hdmaplkr  38472  qsalrel  38548  rntrclfvOAI  38661  ismrcd1  38668  ismrcd2  38669  isnacs3  38680  nacsfix  38682  rgspnid  39146  iocinico  39192  mptrcllem  39314  clcnvlem  39324  dmtrcl  39328  rntrcl  39329  cbviuneq12df  39347  dfrcl2  39360  dftrcl3  39406  brtrclfv2  39413  dfrtrcl3  39419  scottrankd  39937  trivsubgd  39991  trivsubgd2  39992  trivnsgd  39993  nzin  40043  iunincfi  40760  founiiun  40838  founiiun0  40854  inmap  40876  difmapsn  40879  funimaeq  40925  iuneqfzuz  41011  supminfrnmpt  41129  supminfxr2  41155  supminfxrrnmpt  41157  iooiinicc  41228  icomnfinre  41238  iooiinioc  41242  limsupresxr  41457  liminfresxr  41458  limsup10exlem  41463  liminfvalxr  41474  fourierdlem79  41880  rrxsnicc  41995  prsal  42013  issalgend  42031  sge0f1o  42074  caragenuni  42203  caragendifcl  42206  opnvonmbllem2  42325  iinhoiicc  42366  pimconstlt1  42393  pimltpnf  42394  pimiooltgt  42399  pimgtmnf2  42402  pimdecfgtioc  42403  pimincfltioc  42404  pimdecfgtioo  42405  pimincfltioo  42406  preimageiingt  42408  preimaleiinlt  42409  sssmf  42425  smflimlem5  42461  smfmullem4  42479  smfpimbor1lem2  42484  smfsuplem1  42495  fzoopth  42912  sprsymrelf1  43000  lspeqlco  43835  setrecsres  44145