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

Theorem sseq12d 3986
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 3984 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
3 sseq12d.2 . . 3 (𝜑𝐶 = 𝐷)
43sseq2d 3985 . 2 (𝜑 → (𝐵𝐶𝐵𝐷))
52, 4bitrd 282 1 (𝜑 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  wss 3919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-in 3926  df-ss 3936
This theorem is referenced by:  3sstr3d  3999  3sstr4d  4000  ssdifeq0  4415  relcnvtrg  6106  knatar  7103  suppfnss  7851  funsssuppss  7852  smogt  8000  oawordri  8172  omwordi  8193  omwordri  8194  oewordi  8213  oewordri  8214  oeworde  8215  nnawordi  8243  nnmwordi  8257  nnmwordri  8258  sbthlem2  8625  sbth  8634  marypha2lem3  8898  hartogslem1  9003  inf3lem1  9088  tcrank  9310  alephle  9512  cfsmolem  9690  isfin3ds  9749  fin23lem17  9758  fin23lem39  9770  isf32lem1  9773  isf32lem2  9774  isf32lem11  9783  isf33lem  9786  isf34lem7  9799  isf34lem6  9800  fin1a2lem13  9832  itunitc1  9840  dominf  9865  dcomex  9867  axdc2lem  9868  dominfac  9993  fpwwe2cbv  10050  fpwwe2lem2  10052  fpwwecbv  10064  fpwwelem  10065  canthwelem  10070  canthwe  10071  wunex2  10158  swrdval  14005  trcleq2lem  14351  dfrtrcl2  14421  vdwpc  16314  vdwlem1  16315  vdwlem6  16320  vdwlem7  16321  vdwlem8  16322  isstruct2  16493  ressval  16551  mreexexlemd  16915  isacs1i  16928  isssc  17090  ssc2  17092  fullfunc  17176  fthfunc  17177  isps  17812  istsr  17827  isdir  17842  gsumvalx  17886  efgi2  18851  dmdprd  19120  dprdss  19151  dmdprdpr  19171  mhpfval  20798  scmatdmat  21127  basis1  21561  baspartn  21565  eltg  21568  cncls  21885  ispnrm  21950  1stcfb  22056  2ndcctbss  22066  1stcelcls  22072  subislly  22092  kgenidm  22158  ptpjpre1  22182  txcmplem2  22253  flimval  22574  flimcf  22593  fclscf  22636  metss  23121  isngp  23208  iscph  23781  cphsscph  23861  equivcau  23910  caubl  23918  caublcls  23919  ovoliunlem3  24114  volsuplem  24165  volsup  24166  dyaddisj  24206  itg1climres  24324  isausgr  26963  issubgr  27067  subgrprop3  27072  cusgrfilem1  27251  wkslem1  27403  wkslem2  27404  iswlk  27406  wlkres  27466  redwlk  27468  wlkp1lem8  27476  wlkdlem2  27479  crctcshwlkn0lem4  27605  crctcshwlkn0lem5  27606  crctcshwlkn0lem6  27607  2wlkdlem10  27727  3wlkdlem10  27960  eupthseg  27997  issh  28997  isch  29011  hsupss  29130  shslej  29169  shlub  29203  ledi  29329  pjoi0  29506  mdbr4  30087  dmdbr4  30095  dmdi4  30096  dmdbr5  30097  mdslle1i  30106  mdslle2i  30107  mdslmd1lem1  30114  mdslmd1lem2  30115  mdslmd1lem3  30116  mdslmd1lem4  30117  mdslmd1i  30118  sumdmdlem2  30208  resvval  30936  zhmnrg  31268  ispisys  31471  pfxwlk  32430  cvmliftlem3  32594  ismfs  32856  rdgssun  34743  poimirlem32  35037  volsupnfl  35050  elrefrels2  35865  refreleq  35868  elcnvrefrels2  35878  dfsymrels2  35889  dfsymrel2  35893  elsymrels2  35897  symreleq  35902  elrefsymrels2  35913  dftrrels2  35919  dftrrel2  35921  eltrrels2  35923  trreleq  35926  eleqvrels2  35935  lssatle  36259  pmaple  37005  2polcon4bN  37162  ispautN  37343  diaord  38291  dibord  38403  dihord6apre  38500  dihord3  38501  dihord4  38502  dihcnvord  38518  dvh4dimlem  38687  islpolN  38727  mapdordlem2  38881  mapdcnvordN  38902  mapdindp  38915  hdmaplkr  39157  ismrcd1  39559  ismrcd2  39560  ismrc  39562  incssnn0  39572  diophrw  39620  hbtlem5  39992  hbt  39994  rclexi  40235  rtrclex  40237  trclubgNEW  40238  rtrclexi  40241  cnvrcl0  40245  cnvtrcl0  40246  dfrtrcl5  40249  trcleq2lemRP  40250  trficl  40290  dfrcl2  40295  relexpss1d  40326  trclrelexplem  40332  brtrclfv2  40348  dfrtrcl3  40354  heeq12  40398  sscon34b  40645  ntrk2imkb  40663  clsk3nimkb  40666  clsk1independent  40672  isotone1  40674  isotone2  40675  ntrclsss  40689  ntrclsiso  40693  ntrclsk2  40694  ntrclsk3  40696  scottabf  40872  ismnu  40893  nzss  40945  iunincfi  41656  fourierdlem89  42767  fourierdlem90  42768  fourierdlem91  42769  meaiuninclem  43049  meaiunincf  43052  meaiuninc3v  43053  meaiuninc3  43054  meaiininclem  43055  meaiininc  43056  caragenss  43073  carageniuncllem1  43090  ovnsslelem  43129  hoidmvle  43169  ovnhoilem2  43171  hoiqssbl  43194  ovolval5lem2  43222  ovolval5lem3  43223  vonioolem2  43250  vonicclem2  43253  uspgrsprf  44304  scmsuppss  44704
  Copyright terms: Public domain W3C validator