Theorem sseq12d 3382

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 3380	. 2 |- ( ph -> ( A C_ C <-> B C_ C ) )
3		sseq12d.2	. . 3 |- ( ph -> C = D )
4	3	sseq2d 3381	. 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 1364   C_ wss 3325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-in 3332  df-ss 3339

This theorem is referenced by:  3sstr3d  3395  3sstr4d  3396  ssdifeq0  3758  relcnvtr  5354  knatar  6045  suppfnss  6713  funsssuppss  6714  smogt  6824  oawordri  6985  omwordi  7006  omwordri  7007  oewordi  7026  oewordri  7027  oeworde  7028  nnawordi  7056  nnmwordi  7070  nnmwordri  7071  sbthlem2  7418  sbth  7427  marypha2lem3  7683  hartogslem1  7752  inf3lem1  7830  tcrank  8087  alephle  8254  cfsmolem  8435  isfin3ds  8494  fin23lem17  8503  fin23lem39  8515  isf32lem1  8518  isf32lem2  8519  isf32lem11  8528  isf33lem  8531  isf34lem7  8544  isf34lem6  8545  fin1a2lem13  8577  itunitc1  8585  dominf  8610  dcomex  8612  axdc2lem  8613  dominfac  8733  fpwwe2cbv  8793  fpwwe2lem2  8795  fpwwecbv  8807  fpwwelem  8808  canthwelem  8813  canthwe  8814  wunex2  8901  swrdval  12309  vdwpc  14037  vdwlem1  14038  vdwlem6  14043  vdwlem7  14044  vdwlem8  14045  isstruct2  14179  ressval  14221  mreexexlemd  14578  isacs1i  14591  isssc  14729  ssc2  14731  fullfunc  14812  fthfunc  14813  isps  15368  istsr  15383  isdir  15398  gsumvalx  15497  efgi2  16215  dmdprd  16470  dprdss  16516  dmdprdpr  16538  basis1  18514  baspartn  18518  eltg  18521  cncls  18837  ispnrm  18902  1stcfb  19008  2ndcctbss  19018  1stcelcls  19024  subislly  19044  kgenidm  19079  ptpjpre1  19103  txcmplem2  19174  flimval  19495  flimcf  19514  fclscf  19557  metss  20042  isngp  20147  iscph  20648  equivcau  20770  caubl  20777  caublcls  20778  ovoliunlem3  20946  volsuplem  20995  volsup  20996  dyaddisj  21035  itg1climres  21151  isausgra  23213  cusgrafilem1  23322  issh  24545  isch  24560  hsupss  24679  shslej  24718  shlub  24752  ledi  24878  pjoi0  25055  mdbr4  25637  dmdbr4  25645  dmdi4  25646  dmdbr5  25647  mdslle1i  25656  mdslle2i  25657  mdslmd1lem1  25664  mdslmd1lem2  25665  mdslmd1lem3  25666  mdslmd1lem4  25667  mdslmd1i  25668  sumdmdlem2  25758  fpwrelmap  25968  resvval  26231  zhmnrg  26332  cvmliftlem3  27106  dfrtrcl2  27279  volsupnfl  28361  ismrcd1  28959  ismrcd2  28960  ismrc  28962  incssnn0  28972  diophrw  29022  hbtlem5  29409  hbt  29411  scmsuppss  30702  lssatle  32382  pmaple  33127  2polcon4bN  33284  ispautN  33465  diaord  34414  dibord  34526  dihord6apre  34623  dihord3  34624  dihord4  34625  dihcnvord  34641  dvh4dimlem  34810  islpolN  34850  mapdordlem2  35004  mapdcnvordN  35025  mapdindp  35038  hdmaplkr  35283