Theorem eqssd 3265

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ⊆ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  eqrd  3266  eqelssd  3267  unissel  3964  intmin  3990  int0el  4000  pwntru  4336  exmidundif  4343  exmidundifim  4344  dmcosseq  5054  relfld  5316  imadif  5461  imain  5463  fimacnv  5837  fo2ndf  6463  tposeq  6518  tfrlemibfn  6599  tfrlemi14d  6604  tfr1onlembfn  6615  tfri1dALT  6622  tfrcllembfn  6628  dcdifsnid  6777  fisbth  7187  en2eqpr  7214  exmidpw  7215  exmidpweq  7216  undifdcss  7230  nnnninfeq2  7469  en2other2  7548  exmidontriimlem3  7579  pw1m  7583  addnqpr  7928  mulnqpr  7944  distrprg  7955  ltexpri  7980  addcanprg  7983  recexprlemex  8004  aptipr  8008  cauappcvgprlemladd  8025  fzopth  10477  fzosplit  10596  fzouzsplit  10598  zsupssdc  10683  frecuzrdgtcl  10862  frecuzrdgdomlem  10867  ccatrn  11391  phimullem  13023  structcnvcnv  13417  imasaddfnlemg  13684  gsumvallem2  13849  trivsubgd  14052  trivsubgsnd  14053  trivnsgd  14069  kerf1ghm  14126  conjnmz  14131  lspun  14788  lspsn  14802  lspsnneg  14806  lsp0  14809  lsslsp  14815  mulgrhm2  14994  znrrg  15044  eltg4i  15205  unitg  15212  tgtop  15218  tgidm  15224  basgen  15230  2basgeng  15232  epttop  15240  ntrin  15274  isopn3  15275  neiuni  15311  tgrest  15319  resttopon  15321  rest0  15329  txdis  15427  hmeontr  15463  xmettx  15660  ppiqsval  16156  ppinprm  16171  findset  17069  pwtrufal  17125  pwf1oexmid  17127