Theorem sseq12d 3447

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

Syntax hints:   -> wi 4   <-> wb 189   = wceq 1452   C_ wss 3390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-in 3397  df-ss 3404

This theorem is referenced by:  3sstr3d  3460  3sstr4d  3461  ssdifeq0  3841  relcnvtr  5362  knatar  6266  suppfnss  6959  funsssuppss  6960  smogt  7104  oawordri  7269  omwordi  7290  omwordri  7291  oewordi  7310  oewordri  7311  oeworde  7312  nnawordi  7340  nnmwordi  7354  nnmwordri  7355  sbthlem2  7701  sbth  7710  marypha2lem3  7969  hartogslem1  8075  inf3lem1  8151  tcrank  8373  alephle  8537  cfsmolem  8718  isfin3ds  8777  fin23lem17  8786  fin23lem39  8798  isf32lem1  8801  isf32lem2  8802  isf32lem11  8811  isf33lem  8814  isf34lem7  8827  isf34lem6  8828  fin1a2lem13  8860  itunitc1  8868  dominf  8893  dcomex  8895  axdc2lem  8896  dominfac  9016  fpwwe2cbv  9073  fpwwe2lem2  9075  fpwwecbv  9087  fpwwelem  9088  canthwelem  9093  canthwe  9094  wunex2  9181  swrdval  12827  trcleq2lem  13130  dfrtrcl2  13202  vdwpc  15009  vdwlem1  15010  vdwlem6  15015  vdwlem7  15016  vdwlem8  15017  isstruct2  15208  ressval  15254  mreexexlemd  15628  isacs1i  15641  isssc  15803  ssc2  15805  fullfunc  15889  fthfunc  15890  isps  16526  istsr  16541  isdir  16556  gsumvalx  16591  efgi2  17453  dmdprd  17708  dprdss  17740  dmdprdpr  17760  scmatdmat  19617  basis1  20042  baspartn  20046  eltg  20049  cncls  20367  ispnrm  20432  1stcfb  20537  2ndcctbss  20547  1stcelcls  20553  subislly  20573  kgenidm  20639  ptpjpre1  20663  txcmplem2  20734  flimval  21056  flimcf  21075  fclscf  21118  metss  21601  isngp  21688  iscph  22226  equivcau  22348  caubl  22355  caublcls  22356  ovoliunlem3  22535  volsuplem  22587  volsup  22588  dyaddisj  22633  itg1climres  22751  edgss  25158  isausgra  25160  cusgrafilem1  25286  issh  26942  isch  26956  hsupss  27075  shslej  27114  shlub  27148  ledi  27274  pjoi0  27451  mdbr4  28032  dmdbr4  28040  dmdi4  28041  dmdbr5  28042  mdslle1i  28051  mdslle2i  28052  mdslmd1lem1  28059  mdslmd1lem2  28060  mdslmd1lem3  28061  mdslmd1lem4  28062  mdslmd1i  28063  sumdmdlem2  28153  resvval  28664  zhmnrg  28845  ispisys  29048  cvmliftlem3  30082  ismfs  30259  poimirlem32  32036  volsupnfl  32049  lssatle  32652  pmaple  33397  2polcon4bN  33554  ispautN  33735  diaord  34686  dibord  34798  dihord6apre  34895  dihord3  34896  dihord4  34897  dihcnvord  34913  dvh4dimlem  35082  islpolN  35122  mapdordlem2  35276  mapdcnvordN  35297  mapdindp  35310  hdmaplkr  35555  ismrcd1  35611  ismrcd2  35612  ismrc  35614  incssnn0  35624  diophrw  35672  hbtlem5  36058  hbt  36060  rclexi  36293  rtrclex  36295  trclubgNEW  36296  rtrclexi  36299  cnvrcl0  36303  cnvtrcl0  36304  dfrtrcl5  36307  trcleq2lemRP  36308  trficl  36332  dfrcl2  36337  relexpss1d  36368  trclrelexplem  36374  brtrclfv2  36390  dfrtrcl3  36396  heeq12  36442  nzss  36736  fourierdlem89  38171  fourierdlem90  38172  fourierdlem91  38173  caragenss  38444  carageniuncllem1  38461  ovnsslelem  38500  hoidmvle  38540  ovnhoilem2  38542  hoiqssbl  38565  ovolval5lem2  38593  ovolval5lem3  38594  isausgr  39412  issubgr  39507  subgrprop3  39512  cusgrfilem1  39681  is1wlk  39815  1wlk1walk  39838  1wlkres  39866  red1wlk  39868  1wlkp1lem8  39876  1wlkdlem2  39883  crctcsh1wlkn0lem4  39991  crctcsh1wlkn0lem5  39992  crctcsh1wlkn0lem6  39993  crctcsh1wlkn0lem7  39994  crctcsh1wlkn0  39999  11wlkdlem4  40028  21wlkdlem10  40057  31wlkdlem10  40083  eupthseg  40119  scmsuppss  40665