Theorem eqssd 3164

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

Syntax hints:   → wi 4   = wceq 1348   ⊆ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  eqrd  3165  eqelssd  3166  unissel  3825  intmin  3851  int0el  3861  pwntru  4185  exmidundif  4192  exmidundifim  4193  dmcosseq  4882  relfld  5139  imadif  5278  imain  5280  fimacnv  5625  fo2ndf  6206  tposeq  6226  tfrlemibfn  6307  tfrlemi14d  6312  tfr1onlembfn  6323  tfri1dALT  6330  tfrcllembfn  6336  dcdifsnid  6483  fisbth  6861  en2eqpr  6885  exmidpw  6886  exmidpweq  6887  undifdcss  6900  nnnninfeq2  7105  en2other2  7173  exmidontriimlem3  7200  addnqpr  7523  mulnqpr  7539  distrprg  7550  ltexpri  7575  addcanprg  7578  recexprlemex  7599  aptipr  7603  cauappcvgprlemladd  7620  fzopth  10017  fzosplit  10133  fzouzsplit  10135  frecuzrdgtcl  10368  frecuzrdgdomlem  10373  zsupssdc  11909  phimullem  12179  structcnvcnv  12432  eltg4i  12849  unitg  12856  tgtop  12862  tgidm  12868  basgen  12874  2basgeng  12876  epttop  12884  ntrin  12918  isopn3  12919  neiuni  12955  tgrest  12963  resttopon  12965  rest0  12973  txdis  13071  hmeontr  13107  xmettx  13304  findset  13980  pwtrufal  14030  pwf1oexmid  14032