Theorem sseq12d 3463

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3413  df-ss 3420

This theorem is referenced by:  3sstr3d  3476  3sstr4d  3477  ssdifeq0  3852  relcnvtr  5358  knatar  6253  suppfnss  6945  funsssuppss  6946  smogt  7091  oawordri  7256  omwordi  7277  omwordri  7278  oewordi  7297  oewordri  7298  oeworde  7299  nnawordi  7327  nnmwordi  7341  nnmwordri  7342  sbthlem2  7688  sbth  7697  marypha2lem3  7956  hartogslem1  8062  inf3lem1  8138  tcrank  8360  alephle  8524  cfsmolem  8705  isfin3ds  8764  fin23lem17  8773  fin23lem39  8785  isf32lem1  8788  isf32lem2  8789  isf32lem11  8798  isf33lem  8801  isf34lem7  8814  isf34lem6  8815  fin1a2lem13  8847  itunitc1  8855  dominf  8880  dcomex  8882  axdc2lem  8883  dominfac  9003  fpwwe2cbv  9060  fpwwe2lem2  9062  fpwwecbv  9074  fpwwelem  9075  canthwelem  9080  canthwe  9081  wunex2  9168  swrdval  12780  trcleq2lem  13067  dfrtrcl2  13137  vdwpc  14942  vdwlem1  14943  vdwlem6  14948  vdwlem7  14949  vdwlem8  14950  isstruct2  15142  ressval  15188  mreexexlemd  15562  isacs1i  15575  isssc  15737  ssc2  15739  fullfunc  15823  fthfunc  15824  isps  16460  istsr  16475  isdir  16490  gsumvalx  16525  efgi2  17387  dmdprd  17642  dprdss  17674  dmdprdpr  17694  scmatdmat  19552  basis1  19977  baspartn  19981  eltg  19984  cncls  20302  ispnrm  20367  1stcfb  20472  2ndcctbss  20482  1stcelcls  20488  subislly  20508  kgenidm  20574  ptpjpre1  20598  txcmplem2  20669  flimval  20990  flimcf  21009  fclscf  21052  metss  21535  isngp  21622  iscph  22160  equivcau  22282  caubl  22289  caublcls  22290  ovoliunlem3  22469  volsuplem  22520  volsup  22521  dyaddisj  22566  itg1climres  22684  edgss  25091  isausgra  25093  cusgrafilem1  25219  issh  26873  isch  26887  hsupss  27006  shslej  27045  shlub  27079  ledi  27205  pjoi0  27382  mdbr4  27963  dmdbr4  27971  dmdi4  27972  dmdbr5  27973  mdslle1i  27982  mdslle2i  27983  mdslmd1lem1  27990  mdslmd1lem2  27991  mdslmd1lem3  27992  mdslmd1lem4  27993  mdslmd1i  27994  sumdmdlem2  28084  resvval  28602  zhmnrg  28783  ispisys  28986  cvmliftlem3  30022  ismfs  30199  poimirlem32  31984  volsupnfl  31997  lssatle  32593  pmaple  33338  2polcon4bN  33495  ispautN  33676  diaord  34627  dibord  34739  dihord6apre  34836  dihord3  34837  dihord4  34838  dihcnvord  34854  dvh4dimlem  35023  islpolN  35063  mapdordlem2  35217  mapdcnvordN  35238  mapdindp  35251  hdmaplkr  35496  ismrcd1  35552  ismrcd2  35553  ismrc  35555  incssnn0  35565  diophrw  35613  hbtlem5  35999  hbt  36001  rclexi  36234  rtrclex  36236  trclubgNEW  36237  rtrclexi  36240  cnvrcl0  36244  cnvtrcl0  36245  dfrtrcl5  36248  trcleq2lemRP  36249  trficl  36273  dfrcl2  36278  relexpss1d  36309  trclrelexplem  36315  brtrclfv2  36331  dfrtrcl3  36337  heeq12  36383  nzss  36677  fourierdlem89  38069  fourierdlem90  38070  fourierdlem91  38071  caragenss  38335  carageniuncllem1  38352  ovnsslelem  38392  hoidmvle  38432  ovnhoilem2  38434  hoiqssbl  38457  isausgr  39261  issubgr  39353  subgrprop3  39358  cusgrfilem1  39526  is1wlk  39636  1wlk1walk  39656  11wlkdlem4  39739  21wlkdlem4  39760  scmsuppss  40261