Theorem sseq12d 3518

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 3516	. 2 |- ( ph -> ( A C_ C <-> B C_ C ) )
3		sseq12d.2	. . 3 |- ( ph -> C = D )
4	3	sseq2d 3517	. 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 1383   C_ wss 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475

This theorem is referenced by:  3sstr3d  3531  3sstr4d  3532  ssdifeq0  3896  relcnvtr  5517  knatar  6238  suppfnss  6927  funsssuppss  6928  smogt  7040  oawordri  7201  omwordi  7222  omwordri  7223  oewordi  7242  oewordri  7243  oeworde  7244  nnawordi  7272  nnmwordi  7286  nnmwordri  7287  sbthlem2  7630  sbth  7639  marypha2lem3  7899  hartogslem1  7970  inf3lem1  8048  tcrank  8305  alephle  8472  cfsmolem  8653  isfin3ds  8712  fin23lem17  8721  fin23lem39  8733  isf32lem1  8736  isf32lem2  8737  isf32lem11  8746  isf33lem  8749  isf34lem7  8762  isf34lem6  8763  fin1a2lem13  8795  itunitc1  8803  dominf  8828  dcomex  8830  axdc2lem  8831  dominfac  8951  fpwwe2cbv  9011  fpwwe2lem2  9013  fpwwecbv  9025  fpwwelem  9026  canthwelem  9031  canthwe  9032  wunex2  9119  swrdval  12626  vdwpc  14480  vdwlem1  14481  vdwlem6  14486  vdwlem7  14487  vdwlem8  14488  isstruct2  14623  ressval  14666  mreexexlemd  15023  isacs1i  15036  isssc  15171  ssc2  15173  fullfunc  15254  fthfunc  15255  isps  15811  istsr  15826  isdir  15841  gsumvalx  15876  efgi2  16722  dmdprd  17008  dprdss  17055  dmdprdpr  17077  scmatdmat  18995  basis1  19429  baspartn  19433  eltg  19436  cncls  19753  ispnrm  19818  1stcfb  19924  2ndcctbss  19934  1stcelcls  19940  subislly  19960  kgenidm  20026  ptpjpre1  20050  txcmplem2  20121  flimval  20442  flimcf  20461  fclscf  20504  metss  20989  isngp  21094  iscph  21595  equivcau  21717  caubl  21724  caublcls  21725  ovoliunlem3  21893  volsuplem  21943  volsup  21944  dyaddisj  21983  itg1climres  22099  edgss  24330  isausgra  24332  cusgrafilem1  24457  issh  26103  isch  26118  hsupss  26237  shslej  26276  shlub  26310  ledi  26436  pjoi0  26613  mdbr4  27195  dmdbr4  27203  dmdi4  27204  dmdbr5  27205  mdslle1i  27214  mdslle2i  27215  mdslmd1lem1  27222  mdslmd1lem2  27223  mdslmd1lem3  27224  mdslmd1lem4  27225  mdslmd1i  27226  sumdmdlem2  27316  resvval  27795  zhmnrg  27926  cvmliftlem3  28710  ismfs  28887  dfrtrcl2  29049  volsupnfl  30035  ismrcd1  30606  ismrcd2  30607  ismrc  30609  incssnn0  30619  diophrw  30668  hbtlem5  31053  hbt  31055  nzss  31198  fourierdlem89  31932  fourierdlem90  31933  fourierdlem91  31934  scmsuppss  32835  lssatle  34615  pmaple  35360  2polcon4bN  35517  ispautN  35698  diaord  36649  dibord  36761  dihord6apre  36858  dihord3  36859  dihord4  36860  dihcnvord  36876  dvh4dimlem  37045  islpolN  37085  mapdordlem2  37239  mapdcnvordN  37260  mapdindp  37273  hdmaplkr  37518  trficl  37607  trclub  37612  trclubg  37613  heeq12  37622