Theorem sseq12d 3533

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 3531	. 2 |- ( ph -> ( A C_ C <-> B C_ C ) )
3		sseq12d.2	. . 3 |- ( ph -> C = D )
4	3	sseq2d 3532	. 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 1379   C_ wss 3476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490

This theorem is referenced by:  3sstr3d  3546  3sstr4d  3547  ssdifeq0  3909  relcnvtr  5527  knatar  6241  suppfnss  6925  funsssuppss  6926  smogt  7038  oawordri  7199  omwordi  7220  omwordri  7221  oewordi  7240  oewordri  7241  oeworde  7242  nnawordi  7270  nnmwordi  7284  nnmwordri  7285  sbthlem2  7628  sbth  7637  marypha2lem3  7897  hartogslem1  7967  inf3lem1  8045  tcrank  8302  alephle  8469  cfsmolem  8650  isfin3ds  8709  fin23lem17  8718  fin23lem39  8730  isf32lem1  8733  isf32lem2  8734  isf32lem11  8743  isf33lem  8746  isf34lem7  8759  isf34lem6  8760  fin1a2lem13  8792  itunitc1  8800  dominf  8825  dcomex  8827  axdc2lem  8828  dominfac  8948  fpwwe2cbv  9008  fpwwe2lem2  9010  fpwwecbv  9022  fpwwelem  9023  canthwelem  9028  canthwe  9029  wunex2  9116  swrdval  12607  vdwpc  14357  vdwlem1  14358  vdwlem6  14363  vdwlem7  14364  vdwlem8  14365  isstruct2  14499  ressval  14542  mreexexlemd  14899  isacs1i  14912  isssc  15050  ssc2  15052  fullfunc  15133  fthfunc  15134  isps  15689  istsr  15704  isdir  15719  gsumvalx  15824  efgi2  16549  dmdprd  16832  dprdss  16878  dmdprdpr  16900  scmatdmat  18812  basis1  19246  baspartn  19250  eltg  19253  cncls  19569  ispnrm  19634  1stcfb  19740  2ndcctbss  19750  1stcelcls  19756  subislly  19776  kgenidm  19811  ptpjpre1  19835  txcmplem2  19906  flimval  20227  flimcf  20246  fclscf  20289  metss  20774  isngp  20879  iscph  21380  equivcau  21502  caubl  21509  caublcls  21510  ovoliunlem3  21678  volsuplem  21728  volsup  21729  dyaddisj  21768  itg1climres  21884  edgss  24056  isausgra  24058  cusgrafilem1  24183  issh  25829  isch  25844  hsupss  25963  shslej  26002  shlub  26036  ledi  26162  pjoi0  26339  mdbr4  26921  dmdbr4  26929  dmdi4  26930  dmdbr5  26931  mdslle1i  26940  mdslle2i  26941  mdslmd1lem1  26948  mdslmd1lem2  26949  mdslmd1lem3  26950  mdslmd1lem4  26951  mdslmd1i  26952  sumdmdlem2  27042  fpwrelmap  27256  resvval  27508  zhmnrg  27612  cvmliftlem3  28400  dfrtrcl2  28574  volsupnfl  29664  ismrcd1  30262  ismrcd2  30263  ismrc  30265  incssnn0  30275  diophrw  30324  hbtlem5  30709  hbt  30711  nzss  30850  limclner  31221  fourierdlem49  31484  fourierdlem89  31524  fourierdlem90  31525  fourierdlem91  31526  scmsuppss  32064  lssatle  33830  pmaple  34575  2polcon4bN  34732  ispautN  34913  diaord  35862  dibord  35974  dihord6apre  36071  dihord3  36072  dihord4  36073  dihcnvord  36089  dvh4dimlem  36258  islpolN  36298  mapdordlem2  36452  mapdcnvordN  36473  mapdindp  36486  hdmaplkr  36731  trficl  36807  trclub  36812  trclubg  36813