Theorem eqssd 3949

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-in 3905  df-ss 3915

This theorem is referenced by:  eqelssd  3953  uneqdifeq  4437  pweq  4561  unieq  4863  unissel  4886  intmin  4916  unissint  4920  int0el  4927  intidg  5402  dmcosseq  5914  sofld  6125  relfld  6213  preddowncl  6271  frpoind  6281  wfiOLD  6290  tz7.7  6328  fimacnvOLD  7004  knatar  7284  sorpssuni  7647  sorpssint  7648  onint  7703  fo2ndf  8029  suppimacnv  8060  tposeq  8114  frrlem14  8185  onfununi  8242  tfrlem15  8293  oaass  8463  odi  8481  omass  8482  oelim2  8497  oeeui  8504  nnawordex  8539  oaabslem  8548  oaabs2  8550  omabslem  8551  omabs  8552  uniinqs  8657  sucdom2OLD  8947  sucdom2  9071  onomeneq  9093  fineqv  9128  dffi2  9280  fiuni  9285  dffi3  9288  hartogslem1  9399  ixpiunwdom  9447  cantnfp1lem3  9537  oemapvali  9541  cantnf  9550  dfttrcl2  9581  frind  9607  r1val1  9643  rankval3b  9683  rankunb  9707  rankuni2b  9710  rankr1id  9719  rankc2  9728  rankxplim  9736  tcrank  9741  carden2b  9824  harval2  9854  en2other2  9866  infpwfien  9919  coflim  10118  cfcof  10131  cfidm  10132  isf32lem2  10211  fin1a2lem11  10267  fin1a2lem13  10269  ttukeylem7  10372  fpwwe2  10500  winafp  10554  wuncidm  10603  wuncval2  10604  tskuni  10640  grur1  10677  distrpr  10885  ltexpri  10900  reclem4pr  10907  fzopth  13394  fzosplit  13521  fzouzsplit  13523  ccatrn  14393  cotrtrclfv  14822  dmtrclfv  14828  dfrtrcl2  14872  structcnvcnv  16951  imasaddfnlem  17336  imasvscafn  17345  mrcuni  17427  mressmrcd  17433  submrc  17434  ssceq  17635  rescabs  17644  rescabsOLD  17645  setcepi  17900  clatl  18323  ipopos  18351  psdmrn  18388  dirdm  18415  gsumress  18463  gsumvallem2  18569  gsumwspan  18581  trivsubgd  18877  trivsubgsnd  18878  trivnsgd  18896  cycsubg  18923  conjnmz  18964  pmtrprfv  19157  symggen  19174  odf1o2  19274  gex1  19292  sylow2alem1  19318  smndlsmidm  19357  lsmss1  19366  lsmss2  19368  lsmmod  19376  lsmdisj  19382  lsmdisj2  19383  cntzcmn  19536  prmcyg  19590  dmdprdd  19697  dprdspan  19725  dprdres  19726  dprdz  19728  subgdmdprd  19732  subgdprd  19733  dprddisj2  19737  dprd2dlem1  19739  dprd2da  19740  dmdprdsplit2lem  19743  dprdsplit  19746  ablfacrp  19764  pgpfac1lem3  19775  kerf1ghm  20085  issubdrg  20154  lspun  20355  lspsn  20370  lspsnneg  20374  lsp0  20377  lsslsp  20383  lmhmlsp  20417  lspextmo  20424  lsmsp  20454  lspprabs  20463  lspsnvs  20482  lspdisj  20493  lsmcv  20509  lspsnat  20513  lsppratlem6  20520  lspprat  20521  lbsextlem4  20529  lidl1el  20595  drngnidl  20606  lidldvgen  20632  cnsubrg  20764  mulgrhm2  20806  znrrg  20879  ocvin  20985  ocvlsp  20987  mrccss  21005  topsn  22186  eltg4i  22216  unitg  22223  tgtop  22229  tgidm  22236  en2top  22241  basgen  22244  2basgen  22246  fctop  22260  cctop  22262  ppttop  22263  epttop  22265  ntrin  22318  isopn3  22323  opnnei  22377  neiuni  22379  maxlp  22404  clslp  22405  tgrest  22416  resttopon  22418  rest0  22426  restcls  22438  restntr  22439  ordtbas2  22448  ordtbas  22449  ordtrest2  22461  cmpcov2  22647  tgcmp  22658  cmpcld  22659  uncmp  22660  cmpfi  22665  dis2ndc  22717  restnlly  22739  dislly  22754  comppfsc  22789  kgentopon  22795  kgencmp  22802  kgenidm  22804  iskgen2  22805  kgencn3  22815  ptuni2  22833  ptbasfi  22838  xkouni  22856  txcls  22861  txdis  22889  txindis  22891  txcmplem2  22899  xkopt  22912  txconn  22946  qtopval2  22953  qtopuni  22959  qtoprest  22974  qtopomap  22975  qtopcmap  22976  kqsat  22988  kqcldsat  22990  hmeocls  23025  hmeontr  23026  hmphdis  23053  fgfil  23132  fgabs  23136  trfil1  23143  fgtr  23147  uzrest  23154  ufilmax  23164  ufileu  23176  filufint  23177  ufildom1  23183  rnelfm  23210  flimfil  23226  uffclsflim  23288  alexsublem  23301  alexsubALTlem3  23306  alexsubALT  23308  ptcmplem2  23310  ptcmplem3  23311  tgpconncompeqg  23369  haustsms2  23394  tgptsmscls  23407  ust0  23477  ustbas2  23483  iccntr  24090  pi1xfrcnv  24326  clsocv  24520  cfilfcls  24544  equivcmet  24587  hlhil  24713  evthicc2  24730  ovolshft  24781  volsup  24826  dyadmbllem  24869  mbfconstlem  24897  itg11  24961  limciun  25164  dvnres  25201  cpnord  25205  dvcmulf  25215  dvmptcmul  25234  dvcnvre  25289  plyco0  25459  taylthlem1  25638  taylthlem2  25639  ulmdvlem3  25667  wilthlem2  26324  ppisval  26359  ppinprm  26407  chtnprm  26409  sltval2  26910  noextenddif  26922  scutun12  27055  upgrex  27751  uvtxnbgr  28056  cusgredg  28080  ubthlem1  29520  pjhth  30043  ococin  30058  chsupsn  30063  ssjo  30097  chabs1  30166  spansncvi  30302  mdslj1i  30969  mdslj2i  30970  atomli  31032  atcvatlem  31035  atcvat3i  31046  sumdmdlem  31068  difininv  31152  fnpreimac  31295  pmtrcnelor  31647  cycpmrn  31697  fldgenid  31790  1fldgenq  31793  rspidlid  31867  0ringidl  31902  dimkerim  32006  cmpcref  32098  zarcls1  32117  zarclssn  32121  zart0  32127  zarcmplem  32129  xpinpreima2  32155  ordtrest2NEW  32171  sigagenid  32417  imambfm  32529  reprinfz1  32902  bnj1136  33276  bnj1398  33313  bnj1408  33315  bnj1498  33340  fineqvacALT  33366  sconnpi1  33500  cvmliftlem15  33559  madebdaylemlrcut  34175  cofcut1  34186  altopthsn  34359  opnbnd  34610  opnregcld  34615  cldregopn  34616  fnessref  34642  neibastop1  34644  topmeet  34649  topjoin  34650  fnemeet1  34651  fnejoin1  34653  bj-gabeqd  35220  bj-restpw  35376  bj-restb  35378  bj-restuni2  35382  dissneqlem  35624  pibt2  35701  lindsenlbs  35885  poimirlem13  35903  poimirlem14  35904  poimirlem15  35905  fdc  36016  sstotbnd2  36045  isbnd2  36054  totbndbnd  36060  prdstotbnd  36065  heibor1  36081  1idl  36297  igenval2  36337  idreseqidinxp  36583  disjdmqs  37079  lshpdisj  37262  lssats  37287  lsatcvat3  37327  lshpset2N  37394  lfl1dim  37396  lfl1dim2N  37397  lkrpssN  37438  paddass  38114  paddidm  38117  pmod1i  38124  pmapjat1  38129  pclbtwnN  38173  pclunN  38174  paddunN  38203  pclfinclN  38226  dihjust  39493  dihmeetlem1N  39566  dihglblem5apreN  39567  dihmeetlem13N  39595  dochocsp  39655  dochdmj1  39666  dochnoncon  39667  dihjatb  39692  dihjat1lem  39704  lcfl9a  39781  lclkrlem2s  39801  lclkrlem2v  39804  mapdrvallem3  39922  mapdunirnN  39926  mapdin  39938  mapdlsm  39940  baerlem3lem2  39986  baerlem5alem2  39987  baerlem5blem2  39988  hdmaplkr  40189  sticksstones11  40377  rntrclfvOAI  40783  ismrcd1  40790  ismrcd2  40791  isnacs3  40802  nacsfix  40804  rgspnid  41268  iocinico  41315  oacl2g  41325  omabs2  41326  omcl2  41327  ofoaf  41330  harval3  41476  mptrcllem  41551  clcnvlem  41561  dmtrcl  41565  rntrcl  41566  cbviuneq12df  41599  dfrcl2  41612  dftrcl3  41658  brtrclfv2  41665  dfrtrcl3  41671  scottrankd  42196  nzin  42266  iunincfi  42973  founiiun  43051  founiiun0  43064  inmap  43085  difmapsn  43088  funimaeq  43129  iuneqfzuz  43218  supminfrnmpt  43329  supminfxr2  43353  supminfxrrnmpt  43355  pimxrneun  43373  iooiinicc  43425  icomnfinre  43435  iooiinioc  43439  limsupresxr  43652  liminfresxr  43653  limsup10exlem  43658  liminfvalxr  43669  fourierdlem79  44071  rrxsnicc  44186  prsal  44204  issalgend  44222  sge0f1o  44266  caragenuni  44395  caragendifcl  44398  opnvonmbllem2  44517  iinhoiicc  44558  pimconstlt1  44586  pimltpnff  44587  pimiooltgt  44594  pimgtmnf2  44598  pimdecfgtioc  44599  pimincfltioc  44600  pimdecfgtioo  44601  pimincfltioo  44602  preimageiingt  44604  preimaleiinlt  44605  pimgtmnff  44606  sssmf  44622  smflimlem5  44659  smfmullem4  44678  smfpimbor1lem2  44683  smfsuplem1  44695  smfpimne2  44724  fzoopth  45179  sprsymrelf1  45308  lspeqlco  46140  isclatd  46629  intubeu  46630  unilbeu  46631  setrecsres  46767