Theorem sseq12d 3446

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 3444	. 2 |- ( ph -> ( A C_ C <-> B C_ C ) )
3		sseq12d.2	. . 3 |- ( ph -> C = D )
4	3	sseq2d 3445	. 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 1399   C_ wss 3389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-in 3396  df-ss 3403

This theorem is referenced by:  3sstr3d  3459  3sstr4d  3460  ssdifeq0  3826  relcnvtr  5435  knatar  6154  suppfnss  6843  funsssuppss  6844  smogt  6956  oawordri  7117  omwordi  7138  omwordri  7139  oewordi  7158  oewordri  7159  oeworde  7160  nnawordi  7188  nnmwordi  7202  nnmwordri  7203  sbthlem2  7547  sbth  7556  marypha2lem3  7812  hartogslem1  7882  inf3lem1  7959  tcrank  8215  alephle  8382  cfsmolem  8563  isfin3ds  8622  fin23lem17  8631  fin23lem39  8643  isf32lem1  8646  isf32lem2  8647  isf32lem11  8656  isf33lem  8659  isf34lem7  8672  isf34lem6  8673  fin1a2lem13  8705  itunitc1  8713  dominf  8738  dcomex  8740  axdc2lem  8741  dominfac  8861  fpwwe2cbv  8919  fpwwe2lem2  8921  fpwwecbv  8933  fpwwelem  8934  canthwelem  8939  canthwe  8940  wunex2  9027  swrdval  12553  trcleq2lem  12829  dfrtrcl2  12897  vdwpc  14500  vdwlem1  14501  vdwlem6  14506  vdwlem7  14507  vdwlem8  14508  isstruct2  14643  ressval  14688  mreexexlemd  15051  isacs1i  15064  isssc  15226  ssc2  15228  fullfunc  15312  fthfunc  15313  isps  15949  istsr  15964  isdir  15979  gsumvalx  16014  efgi2  16860  dmdprd  17142  dprdss  17189  dmdprdpr  17211  scmatdmat  19102  basis1  19536  baspartn  19540  eltg  19543  cncls  19861  ispnrm  19926  1stcfb  20031  2ndcctbss  20041  1stcelcls  20047  subislly  20067  kgenidm  20133  ptpjpre1  20157  txcmplem2  20228  flimval  20549  flimcf  20568  fclscf  20611  metss  21096  isngp  21201  iscph  21702  equivcau  21824  caubl  21831  caublcls  21832  ovoliunlem3  22000  volsuplem  22050  volsup  22051  dyaddisj  22090  itg1climres  22206  edgss  24473  isausgra  24475  cusgrafilem1  24600  issh  26242  isch  26257  hsupss  26376  shslej  26415  shlub  26449  ledi  26575  pjoi0  26752  mdbr4  27333  dmdbr4  27341  dmdi4  27342  dmdbr5  27343  mdslle1i  27352  mdslle2i  27353  mdslmd1lem1  27360  mdslmd1lem2  27361  mdslmd1lem3  27362  mdslmd1lem4  27363  mdslmd1i  27364  sumdmdlem2  27454  resvval  27971  zhmnrg  28101  ispisys  28301  cvmliftlem3  28921  ismfs  29098  volsupnfl  30224  ismrcd1  30796  ismrcd2  30797  ismrc  30799  incssnn0  30809  diophrw  30857  hbtlem5  31245  hbt  31247  nzss  31390  fourierdlem89  32144  fourierdlem90  32145  fourierdlem91  32146  scmsuppss  33165  lssatle  35153  pmaple  35898  2polcon4bN  36055  ispautN  36236  diaord  37187  dibord  37299  dihord6apre  37396  dihord3  37397  dihord4  37398  dihcnvord  37414  dvh4dimlem  37583  islpolN  37623  mapdordlem2  37777  mapdcnvordN  37798  mapdindp  37811  hdmaplkr  38056  trficl  38204  dfrcl2  38211  dfrtrcl3  38232  relexpss1d  38235  trclrelexplem  38247  brtrclfv2  38258  heeq12  38270