Theorem sseq12d 3634

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

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  3sstr3d  3647  3sstr4d  3648  ssdifeq0  4051  relcnvtr  5655  knatar  6607  suppfnss  7320  funsssuppss  7321  smogt  7464  oawordri  7630  omwordi  7651  omwordri  7652  oewordi  7671  oewordri  7672  oeworde  7673  nnawordi  7701  nnmwordi  7715  nnmwordri  7716  sbthlem2  8071  sbth  8080  marypha2lem3  8343  hartogslem1  8447  inf3lem1  8525  tcrank  8747  alephle  8911  cfsmolem  9092  isfin3ds  9151  fin23lem17  9160  fin23lem39  9172  isf32lem1  9175  isf32lem2  9176  isf32lem11  9185  isf33lem  9188  isf34lem7  9201  isf34lem6  9202  fin1a2lem13  9234  itunitc1  9242  dominf  9267  dcomex  9269  axdc2lem  9270  dominfac  9395  fpwwe2cbv  9452  fpwwe2lem2  9454  fpwwecbv  9466  fpwwelem  9467  canthwelem  9472  canthwe  9473  wunex2  9560  swrdval  13417  trcleq2lem  13730  dfrtrcl2  13802  vdwpc  15684  vdwlem1  15685  vdwlem6  15690  vdwlem7  15691  vdwlem8  15692  isstruct2  15867  ressval  15927  mreexexlemd  16304  isacs1i  16318  isssc  16480  ssc2  16482  fullfunc  16566  fthfunc  16567  isps  17202  istsr  17217  isdir  17232  gsumvalx  17270  efgi2  18138  dmdprd  18397  dprdss  18428  dmdprdpr  18448  scmatdmat  20321  basis1  20754  baspartn  20758  eltg  20761  cncls  21078  ispnrm  21143  1stcfb  21248  2ndcctbss  21258  1stcelcls  21264  subislly  21284  kgenidm  21350  ptpjpre1  21374  txcmplem2  21445  flimval  21767  flimcf  21786  fclscf  21829  metss  22313  isngp  22400  iscph  22970  equivcau  23098  caubl  23106  caublcls  23107  ovoliunlem3  23272  volsuplem  23323  volsup  23324  dyaddisj  23364  itg1climres  23481  isausgr  26059  issubgr  26163  subgrprop3  26168  cusgrfilem1  26351  wkslem1  26503  wkslem2  26504  iswlk  26506  wlkres  26567  redwlk  26569  wlkp1lem8  26577  wlkdlem2  26580  crctcshwlkn0lem4  26705  crctcshwlkn0lem5  26706  crctcshwlkn0lem6  26707  2wlkdlem10  26831  3wlkdlem10  27029  eupthseg  27066  issh  28065  isch  28079  hsupss  28200  shslej  28239  shlub  28273  ledi  28399  pjoi0  28576  mdbr4  29157  dmdbr4  29165  dmdi4  29166  dmdbr5  29167  mdslle1i  29176  mdslle2i  29177  mdslmd1lem1  29184  mdslmd1lem2  29185  mdslmd1lem3  29186  mdslmd1lem4  29187  mdslmd1i  29188  sumdmdlem2  29278  resvval  29827  zhmnrg  30011  ispisys  30215  cvmliftlem3  31269  ismfs  31446  poimirlem32  33441  volsupnfl  33454  lssatle  34302  pmaple  35047  2polcon4bN  35204  ispautN  35385  diaord  36336  dibord  36448  dihord6apre  36545  dihord3  36546  dihord4  36547  dihcnvord  36563  dvh4dimlem  36732  islpolN  36772  mapdordlem2  36926  mapdcnvordN  36947  mapdindp  36960  hdmaplkr  37205  ismrcd1  37261  ismrcd2  37262  ismrc  37264  incssnn0  37274  diophrw  37322  hbtlem5  37698  hbt  37700  rclexi  37922  rtrclex  37924  trclubgNEW  37925  rtrclexi  37928  cnvrcl0  37932  cnvtrcl0  37933  dfrtrcl5  37936  trcleq2lemRP  37937  trficl  37961  dfrcl2  37966  relexpss1d  37997  trclrelexplem  38003  brtrclfv2  38019  dfrtrcl3  38025  heeq12  38070  sscon34b  38317  ntrk2imkb  38335  clsk3nimkb  38338  clsk1independent  38344  isotone1  38346  isotone2  38347  ntrclsss  38361  ntrclsiso  38365  ntrclsk2  38366  ntrclsk3  38368  nzss  38516  iunincfi  39272  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  meaiuninclem  40697  meaiininclem  40700  meaiininc  40701  caragenss  40718  carageniuncllem1  40735  ovnsslelem  40774  hoidmvle  40814  ovnhoilem2  40816  hoiqssbl  40839  ovolval5lem2  40867  ovolval5lem3  40868  vonioolem2  40895  vonicclem2  40898  uspgrsprf  41754  scmsuppss  42153