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  4338  exmidundif  4345  exmidundifim  4346  dmcosseq  5056  relfld  5319  imadif  5464  imain  5466  fimacnv  5840  fo2ndf  6467  tposeq  6522  tfrlemibfn  6603  tfrlemi14d  6608  tfr1onlembfn  6619  tfri1dALT  6626  tfrcllembfn  6632  dcdifsnid  6781  fisbth  7191  en2eqpr  7218  exmidpw  7219  exmidpweq  7220  undifdcss  7234  nnnninfeq2  7475  en2other2  7554  exmidontriimlem3  7585  pw1m  7589  addnqpr  7934  mulnqpr  7950  distrprg  7961  ltexpri  7986  addcanprg  7989  recexprlemex  8010  aptipr  8014  cauappcvgprlemladd  8031  fzopth  10484  fzosplit  10603  fzouzsplit  10605  zsupssdc  10690  frecuzrdgtcl  10870  frecuzrdgdomlem  10875  ccatrn  11399  phimullem  13032  structcnvcnv  13426  imasaddfnlemg  13694  gsumvallem2  13859  trivsubgd  14062  trivsubgsnd  14063  trivnsgd  14079  kerf1ghm  14136  conjnmz  14141  lspun  14848  lspsn  14862  lspsnneg  14866  lsp0  14869  lsslsp  14875  mulgrhm2  15054  znrrg  15104  eltg4i  15281  unitg  15288  tgtop  15294  tgidm  15300  basgen  15306  2basgeng  15308  epttop  15316  ntrin  15350  isopn3  15351  neiuni  15387  tgrest  15395  resttopon  15397  rest0  15405  txdis  15503  hmeontr  15539  xmettx  15736  ppiqsval  16240  ppinprm  16260  chtnprm  16262  findset  17176  pwtrufal  17232  pwf1oexmid  17234