Theorem eqssd 3932

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

Syntax hints:   → wi 4   = wceq 1538   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  eqelssd  3936  uneqdifeq  4396  pweq  4513  unieq  4811  unissel  4831  intmin  4858  unissint  4862  int0el  4869  dmcosseq  5809  sofld  6011  relfld  6094  preddowncl  6143  wfi  6149  tz7.7  6185  fimacnv  6816  knatar  7089  sorpssuni  7438  sorpssint  7439  onint  7490  fo2ndf  7800  suppimacnv  7824  tposeq  7877  onfununi  7961  tfrlem15  8011  oaass  8170  odi  8188  omass  8189  oelim2  8204  oeeui  8211  nnawordex  8246  oaabslem  8253  oaabs2  8255  omabslem  8256  omabs  8257  uniinqs  8360  sucdom2  8610  fineqv  8717  dffi2  8871  fiuni  8876  dffi3  8879  hartogslem1  8990  ixpiunwdom  9038  cantnfp1lem3  9127  oemapvali  9131  cantnf  9140  r1val1  9199  rankval3b  9239  rankunb  9263  rankuni2b  9266  rankr1id  9275  rankc2  9284  rankxplim  9292  tcrank  9297  carden2b  9380  harval2  9410  en2other2  9420  infpwfien  9473  coflim  9672  cfcof  9685  cfidm  9686  isf32lem2  9765  fin1a2lem11  9821  fin1a2lem13  9823  ttukeylem7  9926  fpwwe2  10054  winafp  10108  wuncidm  10157  wuncval2  10158  tskuni  10194  grur1  10231  distrpr  10439  ltexpri  10454  reclem4pr  10461  fzopth  12939  fzosplit  13065  fzouzsplit  13067  ccatrn  13934  cotrtrclfv  14363  dmtrclfv  14369  dfrtrcl2  14413  structcnvcnv  16489  imasaddfnlem  16793  imasvscafn  16802  mrcuni  16884  mressmrcd  16890  submrc  16891  ssceq  17088  rescabs  17095  setcepi  17340  clatl  17718  ipopos  17762  psdmrn  17809  dirdm  17836  gsumress  17884  gsumvallem2  17990  gsumwspan  18003  trivsubgd  18297  trivsubgsnd  18298  trivnsgd  18316  cycsubg  18343  conjnmz  18384  pmtrprfv  18573  symggen  18590  odf1o2  18690  gex1  18708  sylow2alem1  18734  smndlsmidm  18773  lsmidmOLD  18781  lsmss1  18783  lsmss2  18785  lsmmod  18793  lsmdisj  18799  lsmdisj2  18800  cntzcmn  18953  prmcyg  19007  dmdprdd  19114  dprdspan  19142  dprdres  19143  dprdz  19145  subgdmdprd  19149  subgdprd  19150  dprddisj2  19154  dprd2dlem1  19156  dprd2da  19157  dmdprdsplit2lem  19160  dprdsplit  19163  ablfacrp  19181  pgpfac1lem3  19192  kerf1ghm  19491  issubdrg  19553  lspun  19752  lspsn  19767  lspsnneg  19771  lsp0  19774  lsslsp  19780  lmhmlsp  19814  lspextmo  19821  lsmsp  19851  lspprabs  19860  lspsnvs  19879  lspdisj  19890  lsmcv  19906  lspsnat  19910  lsppratlem6  19917  lspprat  19918  lbsextlem4  19926  lidl1el  19984  drngnidl  19995  lidldvgen  20021  cnsubrg  20151  mulgrhm2  20192  znrrg  20257  ocvin  20363  ocvlsp  20365  mrccss  20383  topsn  21536  eltg4i  21565  unitg  21572  tgtop  21578  tgidm  21585  en2top  21590  basgen  21593  2basgen  21595  fctop  21609  cctop  21611  ppttop  21612  epttop  21614  ntrin  21666  isopn3  21671  opnnei  21725  neiuni  21727  maxlp  21752  clslp  21753  tgrest  21764  resttopon  21766  rest0  21774  restcls  21786  restntr  21787  ordtbas2  21796  ordtbas  21797  ordtrest2  21809  cmpcov2  21995  tgcmp  22006  cmpcld  22007  uncmp  22008  cmpfi  22013  dis2ndc  22065  restnlly  22087  dislly  22102  comppfsc  22137  kgentopon  22143  kgencmp  22150  kgenidm  22152  iskgen2  22153  kgencn3  22163  ptuni2  22181  ptbasfi  22186  xkouni  22204  txcls  22209  txdis  22237  txindis  22239  txcmplem2  22247  xkopt  22260  txconn  22294  qtopval2  22301  qtopuni  22307  qtoprest  22322  qtopomap  22323  qtopcmap  22324  kqsat  22336  kqcldsat  22338  hmeocls  22373  hmeontr  22374  hmphdis  22401  fgfil  22480  fgabs  22484  trfil1  22491  fgtr  22495  uzrest  22502  ufilmax  22512  ufileu  22524  filufint  22525  ufildom1  22531  rnelfm  22558  flimfil  22574  uffclsflim  22636  alexsublem  22649  alexsubALTlem3  22654  alexsubALT  22656  ptcmplem2  22658  ptcmplem3  22659  tgpconncompeqg  22717  haustsms2  22742  tgptsmscls  22755  ust0  22825  ustbas2  22831  iccntr  23426  pi1xfrcnv  23662  clsocv  23854  cfilfcls  23878  equivcmet  23921  hlhil  24047  evthicc2  24064  ovolshft  24115  volsup  24160  dyadmbllem  24203  mbfconstlem  24231  itg11  24295  limciun  24497  dvnres  24534  cpnord  24538  dvcmulf  24548  dvmptcmul  24567  dvcnvre  24622  plyco0  24789  taylthlem1  24968  taylthlem2  24969  ulmdvlem3  24997  wilthlem2  25654  ppisval  25689  ppinprm  25737  chtnprm  25739  upgrex  26885  uvtxnbgr  27190  cusgredg  27214  ubthlem1  28653  pjhth  29176  ococin  29191  chsupsn  29196  ssjo  29230  chabs1  29299  spansncvi  29435  mdslj1i  30102  mdslj2i  30103  atomli  30165  atcvatlem  30168  atcvat3i  30179  sumdmdlem  30201  difininv  30288  fnpreimac  30434  pmtrcnelor  30785  cycpmrn  30835  rspidlid  30990  0ringidl  31013  dimkerim  31111  cmpcref  31203  zarcls1  31222  zarclssn  31226  zart0  31232  zarcmplem  31234  xpinpreima2  31260  ordtrest2NEW  31276  sigagenid  31520  imambfm  31630  reprinfz1  32003  bnj1136  32379  bnj1398  32416  bnj1408  32418  bnj1498  32443  sconnpi1  32599  cvmliftlem15  32658  dftrpred3g  33185  trpredpo  33187  frpoind  33193  frind  33198  frrlem14  33249  sltval2  33276  noextenddif  33288  scutun12  33384  altopthsn  33535  opnbnd  33786  opnregcld  33791  cldregopn  33792  fnessref  33818  neibastop1  33820  topmeet  33825  topjoin  33826  fnemeet1  33827  fnejoin1  33829  bj-restpw  34507  bj-restb  34509  bj-restuni2  34513  dissneqlem  34757  pibt2  34834  lindsenlbs  35052  poimirlem13  35070  poimirlem14  35071  poimirlem15  35072  fdc  35183  sstotbnd2  35212  isbnd2  35221  totbndbnd  35227  prdstotbnd  35232  heibor1  35248  1idl  35464  igenval2  35504  idreseqidinxp  35727  lshpdisj  36283  lssats  36308  lsatcvat3  36348  lshpset2N  36415  lfl1dim  36417  lfl1dim2N  36418  lkrpssN  36459  paddass  37134  paddidm  37137  pmod1i  37144  pmapjat1  37149  pclbtwnN  37193  pclunN  37194  paddunN  37223  pclfinclN  37246  dihjust  38513  dihmeetlem1N  38586  dihglblem5apreN  38587  dihmeetlem13N  38615  dochocsp  38675  dochdmj1  38686  dochnoncon  38687  dihjatb  38712  dihjat1lem  38724  lcfl9a  38801  lclkrlem2s  38821  lclkrlem2v  38824  mapdrvallem3  38942  mapdunirnN  38946  mapdin  38958  mapdlsm  38960  baerlem3lem2  39006  baerlem5alem2  39007  baerlem5blem2  39008  hdmaplkr  39209  rntrclfvOAI  39632  ismrcd1  39639  ismrcd2  39640  isnacs3  39651  nacsfix  39653  rgspnid  40116  iocinico  40162  harval3  40244  mptrcllem  40313  clcnvlem  40323  dmtrcl  40327  rntrcl  40328  cbviuneq12df  40362  dfrcl2  40375  dftrcl3  40421  brtrclfv2  40428  dfrtrcl3  40434  scottrankd  40956  nzin  41022  iunincfi  41730  founiiun  41803  founiiun0  41817  inmap  41838  difmapsn  41841  funimaeq  41884  iuneqfzuz  41967  supminfrnmpt  42082  supminfxr2  42108  supminfxrrnmpt  42110  iooiinicc  42179  icomnfinre  42189  iooiinioc  42193  limsupresxr  42408  liminfresxr  42409  limsup10exlem  42414  liminfvalxr  42425  fourierdlem79  42827  rrxsnicc  42942  prsal  42960  issalgend  42978  sge0f1o  43021  caragenuni  43150  caragendifcl  43153  opnvonmbllem2  43272  iinhoiicc  43313  pimconstlt1  43340  pimltpnf  43341  pimiooltgt  43346  pimgtmnf2  43349  pimdecfgtioc  43350  pimincfltioc  43351  pimdecfgtioo  43352  pimincfltioo  43353  preimageiingt  43355  preimaleiinlt  43356  sssmf  43372  smflimlem5  43408  smfmullem4  43426  smfpimbor1lem2  43431  smfsuplem1  43442  fzoopth  43884  sprsymrelf1  44013  lspeqlco  44848  setrecsres  45231