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

Theorem sseq12d 3831
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 3829 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
3 sseq12d.2 . . 3 (𝜑𝐶 = 𝐷)
43sseq2d 3830 . 2 (𝜑 → (𝐵𝐶𝐵𝐷))
52, 4bitrd 270 1 (𝜑 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1637  wss 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-in 3776  df-ss 3783
This theorem is referenced by:  3sstr3d  3844  3sstr4d  3845  ssdifeq0  4247  relcnvtr  5869  knatar  6827  suppfnss  7550  suppfnssOLD  7551  funsssuppss  7552  smogt  7696  oawordri  7863  omwordi  7884  omwordri  7885  oewordi  7904  oewordri  7905  oeworde  7906  nnawordi  7934  nnmwordi  7948  nnmwordri  7949  sbthlem2  8306  sbth  8315  marypha2lem3  8578  hartogslem1  8682  inf3lem1  8768  tcrank  8990  alephle  9190  cfsmolem  9373  isfin3ds  9432  fin23lem17  9441  fin23lem39  9453  isf32lem1  9456  isf32lem2  9457  isf32lem11  9466  isf33lem  9469  isf34lem7  9482  isf34lem6  9483  fin1a2lem13  9515  itunitc1  9523  dominf  9548  dcomex  9550  axdc2lem  9551  dominfac  9676  fpwwe2cbv  9733  fpwwe2lem2  9735  fpwwecbv  9747  fpwwelem  9748  canthwelem  9753  canthwe  9754  wunex2  9841  swrdval  13636  trcleq2lem  13951  dfrtrcl2  14021  vdwpc  15897  vdwlem1  15898  vdwlem6  15903  vdwlem7  15904  vdwlem8  15905  isstruct2  16074  ressval  16134  mreexexlemd  16505  isacs1i  16518  isssc  16680  ssc2  16682  fullfunc  16766  fthfunc  16767  isps  17403  istsr  17418  isdir  17433  gsumvalx  17471  efgi2  18335  dmdprd  18595  dprdss  18626  dmdprdpr  18646  scmatdmat  20528  basis1  20964  baspartn  20968  eltg  20971  cncls  21288  ispnrm  21353  1stcfb  21458  2ndcctbss  21468  1stcelcls  21474  subislly  21494  kgenidm  21560  ptpjpre1  21584  txcmplem2  21655  flimval  21976  flimcf  21995  fclscf  22038  metss  22522  isngp  22609  iscph  23178  equivcau  23306  caubl  23314  caublcls  23315  ovoliunlem3  23481  volsuplem  23532  volsup  23533  dyaddisj  23573  itg1climres  23691  isausgr  26270  issubgr  26375  subgrprop3  26380  cusgrfilem1  26575  wkslem1  26727  wkslem2  26728  iswlk  26730  wlkres  26791  redwlk  26793  wlkp1lem8  26801  wlkdlem2  26804  crctcshwlkn0lem4  26930  crctcshwlkn0lem5  26931  crctcshwlkn0lem6  26932  2wlkdlem10  27071  3wlkdlem10  27338  eupthseg  27375  issh  28389  isch  28403  hsupss  28524  shslej  28563  shlub  28597  ledi  28723  pjoi0  28900  mdbr4  29481  dmdbr4  29489  dmdi4  29490  dmdbr5  29491  mdslle1i  29500  mdslle2i  29501  mdslmd1lem1  29508  mdslmd1lem2  29509  mdslmd1lem3  29510  mdslmd1lem4  29511  mdslmd1i  29512  sumdmdlem2  29602  resvval  30148  zhmnrg  30332  ispisys  30536  cvmliftlem3  31587  ismfs  31764  poimirlem32  33749  volsupnfl  33762  elrefrels2  34575  refreleq  34578  elcnvrefrels2  34588  dfsymrels2  34599  dfsymrel2  34603  elsymrels2  34607  symreleq  34612  elrefsymrels2  34623  lssatle  34790  pmaple  35536  2polcon4bN  35693  ispautN  35874  diaord  36822  dibord  36934  dihord6apre  37031  dihord3  37032  dihord4  37033  dihcnvord  37049  dvh4dimlem  37218  islpolN  37258  mapdordlem2  37412  mapdcnvordN  37433  mapdindp  37446  hdmaplkr  37688  ismrcd1  37757  ismrcd2  37758  ismrc  37760  incssnn0  37770  diophrw  37818  hbtlem5  38193  hbt  38195  rclexi  38416  rtrclex  38418  trclubgNEW  38419  rtrclexi  38422  cnvrcl0  38426  cnvtrcl0  38427  dfrtrcl5  38430  trcleq2lemRP  38431  trficl  38455  dfrcl2  38460  relexpss1d  38491  trclrelexplem  38497  brtrclfv2  38513  dfrtrcl3  38519  heeq12  38564  sscon34b  38811  ntrk2imkb  38829  clsk3nimkb  38832  clsk1independent  38838  isotone1  38840  isotone2  38841  ntrclsss  38855  ntrclsiso  38859  ntrclsk2  38860  ntrclsk3  38862  nzss  39010  iunincfi  39759  fourierdlem89  40885  fourierdlem90  40886  fourierdlem91  40887  meaiuninclem  41170  meaiunincf  41173  meaiuninc3v  41174  meaiuninc3  41175  meaiininclem  41176  meaiininc  41177  caragenss  41194  carageniuncllem1  41211  ovnsslelem  41250  hoidmvle  41290  ovnhoilem2  41292  hoiqssbl  41315  ovolval5lem2  41343  ovolval5lem3  41344  vonioolem2  41371  vonicclem2  41374  uspgrsprf  42316  scmsuppss  42715
  Copyright terms: Public domain W3C validator