Theorem sseq12d 3337

Description: An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999.)

Hypotheses

Ref	Expression
sseq1d.1	|- ( ph -> A = B )
sseq12d.2	|- ( ph -> C = D )

Assertion

Ref	Expression
sseq12d	|- ( ph -> ( A C_ C <-> B C_ D ) )

Proof of Theorem sseq12d

Step	Hyp	Ref	Expression
1		sseq1d.1	. . 3 |- ( ph -> A = B )
2	1	sseq1d 3335	. 2 |- ( ph -> ( A C_ C <-> B C_ C ) )
3		sseq12d.2	. . 3 |- ( ph -> C = D )
4	3	sseq2d 3336	. 2 |- ( ph -> ( B C_ C <-> B C_ D ) )
5	2, 4	bitrd 245	1 |- ( ph -> ( A C_ C <-> B C_ D ) )

Syntax hints:   -> wi 4   <-> wb 177   = wceq 1649   C_ wss 3280

This theorem is referenced by:  3sstr3d  3350  3sstr4d  3351  ssdifeq0  3670  relcnvtr  5348  knatar  6039  smogt  6588  oawordri  6752  omwordi  6773  omwordri  6774  oewordi  6793  oewordri  6794  oeworde  6795  nnawordi  6823  nnmwordi  6837  nnmwordri  6838  sbthlem2  7177  sbth  7186  marypha2lem3  7400  hartogslem1  7467  inf3lem1  7539  tcrank  7764  alephle  7925  cfsmolem  8106  isfin3ds  8165  fin23lem17  8174  fin23lem39  8186  isf32lem1  8189  isf32lem2  8190  isf32lem11  8199  isf33lem  8202  isf34lem7  8215  isf34lem6  8216  fin1a2lem13  8248  itunitc1  8256  dominf  8281  dcomex  8283  axdc2lem  8284  dominfac  8404  fpwwe2cbv  8461  fpwwe2lem2  8463  fpwwecbv  8475  fpwwelem  8476  canthwelem  8481  canthwe  8482  wunex2  8569  swrdval  11719  vdwpc  13303  vdwlem1  13304  vdwlem6  13309  vdwlem7  13310  vdwlem8  13311  isstruct2  13433  ressval  13471  mreexexlemd  13824  isacs1i  13837  isssc  13975  ssc2  13977  fullfunc  14058  fthfunc  14059  isps  14589  istsr  14604  isdir  14632  gsumvalx  14729  efgi2  15312  dmdprd  15514  dprdss  15542  dmdprdpr  15562  basis1  16970  baspartn  16974  eltg  16977  cncls  17292  ispnrm  17357  1stcfb  17461  2ndcctbss  17471  1stcelcls  17477  subislly  17497  kgenidm  17532  ptpjpre1  17556  txcmplem2  17627  flimval  17948  flimcf  17967  fclscf  18010  metss  18491  isngp  18596  iscph  19086  equivcau  19206  caubl  19213  caublcls  19214  ovoliunlem3  19353  volsuplem  19402  volsup  19403  dyaddisj  19441  itg1climres  19559  isausgra  21332  cusgrafilem1  21441  issh  22663  isch  22678  hsupss  22796  shslej  22835  shlub  22869  ledi  22995  pjoi0  23172  mdbr4  23754  dmdbr4  23762  dmdi4  23763  dmdbr5  23764  mdslle1i  23773  mdslle2i  23774  mdslmd1lem1  23781  mdslmd1lem2  23782  mdslmd1lem3  23783  mdslmd1lem4  23784  mdslmd1i  23785  sumdmdlem2  23875  zhmnrg  24304  cvmliftlem3  24927  dfrtrcl2  25101  volsupnfl  26150  ismrcd1  26642  ismrcd2  26643  ismrc  26645  incssnn0  26655  diophrw  26707  hbtlem5  27200  hbt  27202  lssatle  29498  pmaple  30243  2polcon4bN  30400  ispautN  30581  diaord  31530  dibord  31642  dihord6apre  31739  dihord3  31740  dihord4  31741  dihcnvord  31757  dvh4dimlem  31926  islpolN  31966  mapdordlem2  32120  mapdcnvordN  32141  mapdindp  32154  hdmaplkr  32399

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294