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	|- ( ph -> A C_ B )
eqssd.2	|- ( ph -> B C_ A )

Assertion

Ref	Expression
eqssd	|- ( ph -> A = B )

Proof of Theorem eqssd

Step	Hyp	Ref	Expression
1		eqssd.1	. 2 |- ( ph -> A C_ B )
2		eqssd.2	. 2 |- ( ph -> B C_ A )
3		eqss 3263	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
4	1, 2, 3	sylanbrc 421	1 |- ( ph -> A = B )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   C_ 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  6523  tfrlemibfn  6604  tfrlemi14d  6609  tfr1onlembfn  6620  tfri1dALT  6627  tfrcllembfn  6633  dcdifsnid  6782  fisbth  7193  en2eqpr  7220  exmidpw  7221  exmidpweq  7222  undifdcss  7236  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  10483  fzosplit  10602  fzouzsplit  10604  zsupssdc  10689  frecuzrdgtcl  10869  frecuzrdgdomlem  10874  ccatrn  11398  phimullem  13031  structcnvcnv  13425  imasaddfnlemg  13693  gsumvallem2  13858  trivsubgd  14061  trivsubgsnd  14062  trivnsgd  14078  kerf1ghm  14135  conjnmz  14140  lspun  14847  lspsn  14861  lspsnneg  14865  lsp0  14868  lsslsp  14874  mulgrhm2  15053  znrrg  15103  eltg4i  15298  unitg  15305  tgtop  15311  tgidm  15317  basgen  15323  2basgeng  15325  epttop  15333  ntrin  15367  isopn3  15368  neiuni  15404  tgrest  15412  resttopon  15414  rest0  15422  txdis  15520  hmeontr  15556  xmettx  15753  ppiqsval  16257  ppinprm  16277  chtnprm  16279  findset  17193  pwtrufal  17249  pwf1oexmid  17251