Theorem sseq12d 3385

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 3383	. 2 |- ( ph -> ( A C_ C <-> B C_ C ) )
3		sseq12d.2	. . 3 |- ( ph -> C = D )
4	3	sseq2d 3384	. 2 |- ( ph -> ( B C_ C <-> B C_ D ) )
5	2, 4	bitrd 253	1 |- ( ph -> ( A C_ C <-> B C_ D ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1369   C_ wss 3328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3335  df-ss 3342

This theorem is referenced by:  3sstr3d  3398  3sstr4d  3399  ssdifeq0  3761  relcnvtr  5357  knatar  6048  suppfnss  6714  funsssuppss  6715  smogt  6828  oawordri  6989  omwordi  7010  omwordri  7011  oewordi  7030  oewordri  7031  oeworde  7032  nnawordi  7060  nnmwordi  7074  nnmwordri  7075  sbthlem2  7422  sbth  7431  marypha2lem3  7687  hartogslem1  7756  inf3lem1  7834  tcrank  8091  alephle  8258  cfsmolem  8439  isfin3ds  8498  fin23lem17  8507  fin23lem39  8519  isf32lem1  8522  isf32lem2  8523  isf32lem11  8532  isf33lem  8535  isf34lem7  8548  isf34lem6  8549  fin1a2lem13  8581  itunitc1  8589  dominf  8614  dcomex  8616  axdc2lem  8617  dominfac  8737  fpwwe2cbv  8797  fpwwe2lem2  8799  fpwwecbv  8811  fpwwelem  8812  canthwelem  8817  canthwe  8818  wunex2  8905  swrdval  12313  vdwpc  14041  vdwlem1  14042  vdwlem6  14047  vdwlem7  14048  vdwlem8  14049  isstruct2  14183  ressval  14225  mreexexlemd  14582  isacs1i  14595  isssc  14733  ssc2  14735  fullfunc  14816  fthfunc  14817  isps  15372  istsr  15387  isdir  15402  gsumvalx  15502  efgi2  16222  dmdprd  16480  dprdss  16526  dmdprdpr  16548  basis1  18555  baspartn  18559  eltg  18562  cncls  18878  ispnrm  18943  1stcfb  19049  2ndcctbss  19059  1stcelcls  19065  subislly  19085  kgenidm  19120  ptpjpre1  19144  txcmplem2  19215  flimval  19536  flimcf  19555  fclscf  19598  metss  20083  isngp  20188  iscph  20689  equivcau  20811  caubl  20818  caublcls  20819  ovoliunlem3  20987  volsuplem  21036  volsup  21037  dyaddisj  21076  itg1climres  21192  isausgra  23278  cusgrafilem1  23387  issh  24610  isch  24625  hsupss  24744  shslej  24783  shlub  24817  ledi  24943  pjoi0  25120  mdbr4  25702  dmdbr4  25710  dmdi4  25711  dmdbr5  25712  mdslle1i  25721  mdslle2i  25722  mdslmd1lem1  25729  mdslmd1lem2  25730  mdslmd1lem3  25731  mdslmd1lem4  25732  mdslmd1i  25733  sumdmdlem2  25823  fpwrelmap  26033  resvval  26295  zhmnrg  26396  cvmliftlem3  27176  dfrtrcl2  27350  volsupnfl  28436  ismrcd1  29034  ismrcd2  29035  ismrc  29037  incssnn0  29047  diophrw  29097  hbtlem5  29484  hbt  29486  scmsuppss  30785  lssatle  32660  pmaple  33405  2polcon4bN  33562  ispautN  33743  diaord  34692  dibord  34804  dihord6apre  34901  dihord3  34902  dihord4  34903  dihcnvord  34919  dvh4dimlem  35088  islpolN  35128  mapdordlem2  35282  mapdcnvordN  35303  mapdindp  35316  hdmaplkr  35561