Theorem sseq12d 3495

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

Syntax hints:   -> wi 4   <-> wb 188   = wceq 1438   C_ wss 3438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-in 3445  df-ss 3452

This theorem is referenced by:  3sstr3d  3508  3sstr4d  3509  ssdifeq0  3880  relcnvtr  5373  knatar  6262  suppfnss  6950  funsssuppss  6951  smogt  7096  oawordri  7261  omwordi  7282  omwordri  7283  oewordi  7302  oewordri  7303  oeworde  7304  nnawordi  7332  nnmwordi  7346  nnmwordri  7347  sbthlem2  7691  sbth  7700  marypha2lem3  7959  hartogslem1  8065  inf3lem1  8141  tcrank  8362  alephle  8525  cfsmolem  8706  isfin3ds  8765  fin23lem17  8774  fin23lem39  8786  isf32lem1  8789  isf32lem2  8790  isf32lem11  8799  isf33lem  8802  isf34lem7  8815  isf34lem6  8816  fin1a2lem13  8848  itunitc1  8856  dominf  8881  dcomex  8883  axdc2lem  8884  dominfac  9004  fpwwe2cbv  9061  fpwwe2lem2  9063  fpwwecbv  9075  fpwwelem  9076  canthwelem  9081  canthwe  9082  wunex2  9169  swrdval  12773  trcleq2lem  13053  dfrtrcl2  13123  vdwpc  14927  vdwlem1  14928  vdwlem6  14933  vdwlem7  14934  vdwlem8  14935  isstruct2  15127  ressval  15173  mreexexlemd  15547  isacs1i  15560  isssc  15722  ssc2  15724  fullfunc  15808  fthfunc  15809  isps  16445  istsr  16460  isdir  16475  gsumvalx  16510  efgi2  17372  dmdprd  17627  dprdss  17659  dmdprdpr  17679  scmatdmat  19536  basis1  19961  baspartn  19965  eltg  19968  cncls  20286  ispnrm  20351  1stcfb  20456  2ndcctbss  20466  1stcelcls  20472  subislly  20492  kgenidm  20558  ptpjpre1  20582  txcmplem2  20653  flimval  20974  flimcf  20993  fclscf  21036  metss  21519  isngp  21606  iscph  22144  equivcau  22266  caubl  22273  caublcls  22274  ovoliunlem3  22453  volsuplem  22504  volsup  22505  dyaddisj  22550  itg1climres  22668  edgss  25075  isausgra  25077  cusgrafilem1  25203  issh  26857  isch  26871  hsupss  26990  shslej  27029  shlub  27063  ledi  27189  pjoi0  27366  mdbr4  27947  dmdbr4  27955  dmdi4  27956  dmdbr5  27957  mdslle1i  27966  mdslle2i  27967  mdslmd1lem1  27974  mdslmd1lem2  27975  mdslmd1lem3  27976  mdslmd1lem4  27977  mdslmd1i  27978  sumdmdlem2  28068  resvval  28596  zhmnrg  28777  ispisys  28980  cvmliftlem3  30016  ismfs  30193  poimirlem32  31934  volsupnfl  31947  lssatle  32548  pmaple  33293  2polcon4bN  33450  ispautN  33631  diaord  34582  dibord  34694  dihord6apre  34791  dihord3  34792  dihord4  34793  dihcnvord  34809  dvh4dimlem  34978  islpolN  35018  mapdordlem2  35172  mapdcnvordN  35193  mapdindp  35206  hdmaplkr  35451  ismrcd1  35507  ismrcd2  35508  ismrc  35510  incssnn0  35520  diophrw  35568  hbtlem5  35955  hbt  35957  trficl  36169  dfrcl2  36174  relexpss1d  36205  trclrelexplem  36211  brtrclfv2  36227  dfrtrcl3  36233  heeq12  36277  nzss  36572  fourierdlem89  37927  fourierdlem90  37928  fourierdlem91  37929  caragenss  38152  carageniuncllem1  38169  ovnsslelem  38205  isausgr  38932  scmsuppss  39551