Theorem eqssd 3242

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

Syntax hints:   → wi 4   = wceq 1395   ⊆ wss 3198

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  eqrd  3243  eqelssd  3244  unissel  3920  intmin  3946  int0el  3956  pwntru  4287  exmidundif  4294  exmidundifim  4295  dmcosseq  5002  relfld  5263  imadif  5407  imain  5409  fimacnv  5772  fo2ndf  6387  tposeq  6408  tfrlemibfn  6489  tfrlemi14d  6494  tfr1onlembfn  6505  tfri1dALT  6512  tfrcllembfn  6518  dcdifsnid  6667  fisbth  7065  en2eqpr  7092  exmidpw  7093  exmidpweq  7094  undifdcss  7108  nnnninfeq2  7319  en2other2  7397  exmidontriimlem3  7428  pw1m  7432  addnqpr  7771  mulnqpr  7787  distrprg  7798  ltexpri  7823  addcanprg  7826  recexprlemex  7847  aptipr  7851  cauappcvgprlemladd  7868  fzopth  10286  fzosplit  10404  fzouzsplit  10406  zsupssdc  10488  frecuzrdgtcl  10664  frecuzrdgdomlem  10669  ccatrn  11176  phimullem  12787  structcnvcnv  13088  imasaddfnlemg  13387  gsumvallem2  13566  trivsubgd  13777  trivsubgsnd  13778  trivnsgd  13794  kerf1ghm  13851  conjnmz  13856  lspun  14406  lspsn  14420  lspsnneg  14424  lsp0  14427  lsslsp  14433  mulgrhm2  14614  znrrg  14664  eltg4i  14769  unitg  14776  tgtop  14782  tgidm  14788  basgen  14794  2basgeng  14796  epttop  14804  ntrin  14838  isopn3  14839  neiuni  14875  tgrest  14883  resttopon  14885  rest0  14893  txdis  14991  hmeontr  15027  xmettx  15224  findset  16476  pwtrufal  16534  pwf1oexmid  16536