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  10467  fzosplit  10586  fzouzsplit  10588  zsupssdc  10673  frecuzrdgtcl  10849  frecuzrdgdomlem  10854  ccatrn  11377  phimullem  13003  structcnvcnv  13368  imasaddfnlemg  13635  gsumvallem2  13800  trivsubgd  14003  trivsubgsnd  14004  trivnsgd  14020  kerf1ghm  14077  conjnmz  14082  lspun  14739  lspsn  14753  lspsnneg  14757  lsp0  14760  lsslsp  14766  mulgrhm2  14945  znrrg  14995  eltg4i  15156  unitg  15163  tgtop  15169  tgidm  15175  basgen  15181  2basgeng  15183  epttop  15191  ntrin  15225  isopn3  15226  neiuni  15262  tgrest  15270  resttopon  15272  rest0  15280  txdis  15378  hmeontr  15414  xmettx  15611  findset  16971  pwtrufal  17027  pwf1oexmid  17029