MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sseq12d Structured version   Visualization version   GIF version

Theorem sseq12d 3618
Description: An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999.)
Hypotheses
Ref Expression
sseq1d.1 (𝜑𝐴 = 𝐵)
sseq12d.2 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
sseq12d (𝜑 → (𝐴𝐶𝐵𝐷))

Proof of Theorem sseq12d
StepHypRef Expression
1 sseq1d.1 . . 3 (𝜑𝐴 = 𝐵)
21sseq1d 3616 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
3 sseq12d.2 . . 3 (𝜑𝐶 = 𝐷)
43sseq2d 3617 . 2 (𝜑 → (𝐵𝐶𝐵𝐷))
52, 4bitrd 268 1 (𝜑 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  wss 3559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3566  df-ss 3573
This theorem is referenced by:  3sstr3d  3631  3sstr4d  3632  ssdifeq0  4028  relcnvtr  5619  knatar  6567  suppfnss  7272  funsssuppss  7273  smogt  7416  oawordri  7582  omwordi  7603  omwordri  7604  oewordi  7623  oewordri  7624  oeworde  7625  nnawordi  7653  nnmwordi  7667  nnmwordri  7668  sbthlem2  8023  sbth  8032  marypha2lem3  8295  hartogslem1  8399  inf3lem1  8477  tcrank  8699  alephle  8863  cfsmolem  9044  isfin3ds  9103  fin23lem17  9112  fin23lem39  9124  isf32lem1  9127  isf32lem2  9128  isf32lem11  9137  isf33lem  9140  isf34lem7  9153  isf34lem6  9154  fin1a2lem13  9186  itunitc1  9194  dominf  9219  dcomex  9221  axdc2lem  9222  dominfac  9347  fpwwe2cbv  9404  fpwwe2lem2  9406  fpwwecbv  9418  fpwwelem  9419  canthwelem  9424  canthwe  9425  wunex2  9512  swrdval  13363  trcleq2lem  13672  dfrtrcl2  13744  vdwpc  15619  vdwlem1  15620  vdwlem6  15625  vdwlem7  15626  vdwlem8  15627  isstruct2  15801  ressval  15859  mreexexlemd  16236  isacs1i  16250  isssc  16412  ssc2  16414  fullfunc  16498  fthfunc  16499  isps  17134  istsr  17149  isdir  17164  gsumvalx  17202  efgi2  18070  dmdprd  18329  dprdss  18360  dmdprdpr  18380  scmatdmat  20253  basis1  20678  baspartn  20682  eltg  20685  cncls  21001  ispnrm  21066  1stcfb  21171  2ndcctbss  21181  1stcelcls  21187  subislly  21207  kgenidm  21273  ptpjpre1  21297  txcmplem2  21368  flimval  21690  flimcf  21709  fclscf  21752  metss  22236  isngp  22323  iscph  22893  equivcau  23021  caubl  23029  caublcls  23030  ovoliunlem3  23195  volsuplem  23246  volsup  23247  dyaddisj  23287  itg1climres  23404  isausgr  25969  issubgr  26073  subgrprop3  26078  cusgrfilem1  26255  wkslem1  26390  wkslem2  26391  iswlk  26393  wlkres  26453  redwlk  26455  wlkp1lem8  26463  wlkdlem2  26466  crctcshwlkn0lem4  26591  crctcshwlkn0lem5  26592  crctcshwlkn0lem6  26593  2wlkdlem10  26717  3wlkdlem10  26912  eupthseg  26949  issh  27935  isch  27949  hsupss  28070  shslej  28109  shlub  28143  ledi  28269  pjoi0  28446  mdbr4  29027  dmdbr4  29035  dmdi4  29036  dmdbr5  29037  mdslle1i  29046  mdslle2i  29047  mdslmd1lem1  29054  mdslmd1lem2  29055  mdslmd1lem3  29056  mdslmd1lem4  29057  mdslmd1i  29058  sumdmdlem2  29148  resvval  29636  zhmnrg  29817  ispisys  30020  cvmliftlem3  31012  ismfs  31189  poimirlem32  33108  volsupnfl  33121  lssatle  33817  pmaple  34562  2polcon4bN  34719  ispautN  34900  diaord  35851  dibord  35963  dihord6apre  36060  dihord3  36061  dihord4  36062  dihcnvord  36078  dvh4dimlem  36247  islpolN  36287  mapdordlem2  36441  mapdcnvordN  36462  mapdindp  36475  hdmaplkr  36720  ismrcd1  36776  ismrcd2  36777  ismrc  36779  incssnn0  36789  diophrw  36837  hbtlem5  37214  hbt  37216  rclexi  37438  rtrclex  37440  trclubgNEW  37441  rtrclexi  37444  cnvrcl0  37448  cnvtrcl0  37449  dfrtrcl5  37452  trcleq2lemRP  37453  trficl  37477  dfrcl2  37482  relexpss1d  37513  trclrelexplem  37519  brtrclfv2  37535  dfrtrcl3  37541  heeq12  37587  sscon34b  37834  ntrk2imkb  37852  clsk3nimkb  37855  clsk1independent  37861  isotone1  37863  isotone2  37864  ntrclsss  37878  ntrclsiso  37882  ntrclsk2  37883  ntrclsk3  37885  nzss  38033  iunincfi  38790  fourierdlem89  39745  fourierdlem90  39746  fourierdlem91  39747  meaiuninclem  40030  meaiininclem  40033  meaiininc  40034  caragenss  40051  carageniuncllem1  40068  ovnsslelem  40107  hoidmvle  40147  ovnhoilem2  40149  hoiqssbl  40172  ovolval5lem2  40200  ovolval5lem3  40201  vonioolem2  40228  vonicclem2  40231  uspgrsprf  41068  scmsuppss  41467
  Copyright terms: Public domain W3C validator