Theorem eqssd 3244

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

Syntax hints:   → wi 4   = wceq 1397   ⊆ wss 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  eqrd  3245  eqelssd  3246  unissel  3922  intmin  3948  int0el  3958  pwntru  4289  exmidundif  4296  exmidundifim  4297  dmcosseq  5004  relfld  5265  imadif  5410  imain  5412  fimacnv  5776  fo2ndf  6392  tposeq  6413  tfrlemibfn  6494  tfrlemi14d  6499  tfr1onlembfn  6510  tfri1dALT  6517  tfrcllembfn  6523  dcdifsnid  6672  fisbth  7072  en2eqpr  7099  exmidpw  7100  exmidpweq  7101  undifdcss  7115  nnnninfeq2  7328  en2other2  7407  exmidontriimlem3  7438  pw1m  7442  addnqpr  7781  mulnqpr  7797  distrprg  7808  ltexpri  7833  addcanprg  7836  recexprlemex  7857  aptipr  7861  cauappcvgprlemladd  7878  fzopth  10296  fzosplit  10414  fzouzsplit  10416  zsupssdc  10499  frecuzrdgtcl  10675  frecuzrdgdomlem  10680  ccatrn  11190  phimullem  12802  structcnvcnv  13103  imasaddfnlemg  13402  gsumvallem2  13581  trivsubgd  13792  trivsubgsnd  13793  trivnsgd  13809  kerf1ghm  13866  conjnmz  13871  lspun  14422  lspsn  14436  lspsnneg  14440  lsp0  14443  lsslsp  14449  mulgrhm2  14630  znrrg  14680  eltg4i  14785  unitg  14792  tgtop  14798  tgidm  14804  basgen  14810  2basgeng  14812  epttop  14820  ntrin  14854  isopn3  14855  neiuni  14891  tgrest  14899  resttopon  14901  rest0  14909  txdis  15007  hmeontr  15043  xmettx  15240  findset  16566  pwtrufal  16624  pwf1oexmid  16626