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

Theorem sseq12d 3783
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 3781 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
3 sseq12d.2 . . 3 (𝜑𝐶 = 𝐷)
43sseq2d 3782 . 2 (𝜑 → (𝐵𝐶𝐵𝐷))
52, 4bitrd 268 1 (𝜑 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1631  wss 3723
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-in 3730  df-ss 3737
This theorem is referenced by:  3sstr3d  3796  3sstr4d  3797  ssdifeq0  4193  relcnvtr  5799  knatar  6750  suppfnss  7471  suppfnssOLD  7472  funsssuppss  7473  smogt  7617  oawordri  7784  omwordi  7805  omwordri  7806  oewordi  7825  oewordri  7826  oeworde  7827  nnawordi  7855  nnmwordi  7869  nnmwordri  7870  sbthlem2  8227  sbth  8236  marypha2lem3  8499  hartogslem1  8603  inf3lem1  8689  tcrank  8911  alephle  9111  cfsmolem  9294  isfin3ds  9353  fin23lem17  9362  fin23lem39  9374  isf32lem1  9377  isf32lem2  9378  isf32lem11  9387  isf33lem  9390  isf34lem7  9403  isf34lem6  9404  fin1a2lem13  9436  itunitc1  9444  dominf  9469  dcomex  9471  axdc2lem  9472  dominfac  9597  fpwwe2cbv  9654  fpwwe2lem2  9656  fpwwecbv  9668  fpwwelem  9669  canthwelem  9674  canthwe  9675  wunex2  9762  swrdval  13625  trcleq2lem  13940  dfrtrcl2  14010  vdwpc  15891  vdwlem1  15892  vdwlem6  15897  vdwlem7  15898  vdwlem8  15899  isstruct2  16074  ressval  16134  mreexexlemd  16512  isacs1i  16525  isssc  16687  ssc2  16689  fullfunc  16773  fthfunc  16774  isps  17410  istsr  17425  isdir  17440  gsumvalx  17478  efgi2  18345  dmdprd  18605  dprdss  18636  dmdprdpr  18656  scmatdmat  20539  basis1  20975  baspartn  20979  eltg  20982  cncls  21299  ispnrm  21364  1stcfb  21469  2ndcctbss  21479  1stcelcls  21485  subislly  21505  kgenidm  21571  ptpjpre1  21595  txcmplem2  21666  flimval  21987  flimcf  22006  fclscf  22049  metss  22533  isngp  22620  iscph  23189  equivcau  23317  caubl  23325  caublcls  23326  ovoliunlem3  23492  volsuplem  23543  volsup  23544  dyaddisj  23584  itg1climres  23701  isausgr  26281  issubgr  26386  subgrprop3  26391  cusgrfilem1  26586  wkslem1  26738  wkslem2  26739  iswlk  26741  wlkres  26802  redwlk  26804  wlkp1lem8  26812  wlkdlem2  26815  crctcshwlkn0lem4  26941  crctcshwlkn0lem5  26942  crctcshwlkn0lem6  26943  2wlkdlem10  27082  3wlkdlem10  27349  eupthseg  27386  issh  28405  isch  28419  hsupss  28540  shslej  28579  shlub  28613  ledi  28739  pjoi0  28916  mdbr4  29497  dmdbr4  29505  dmdi4  29506  dmdbr5  29507  mdslle1i  29516  mdslle2i  29517  mdslmd1lem1  29524  mdslmd1lem2  29525  mdslmd1lem3  29526  mdslmd1lem4  29527  mdslmd1i  29528  sumdmdlem2  29618  resvval  30167  zhmnrg  30351  ispisys  30555  cvmliftlem3  31607  ismfs  31784  poimirlem32  33774  volsupnfl  33787  elrefrels2  34609  refreleq  34612  elcnvrefrels2  34622  dfsymrels2  34633  dfsymrel2  34637  elsymrels2  34641  symreleq  34646  elrefsymrels2  34657  lssatle  34824  pmaple  35569  2polcon4bN  35726  ispautN  35907  diaord  36857  dibord  36969  dihord6apre  37066  dihord3  37067  dihord4  37068  dihcnvord  37084  dvh4dimlem  37253  islpolN  37293  mapdordlem2  37447  mapdcnvordN  37468  mapdindp  37481  hdmaplkr  37723  ismrcd1  37787  ismrcd2  37788  ismrc  37790  incssnn0  37800  diophrw  37848  hbtlem5  38224  hbt  38226  rclexi  38448  rtrclex  38450  trclubgNEW  38451  rtrclexi  38454  cnvrcl0  38458  cnvtrcl0  38459  dfrtrcl5  38462  trcleq2lemRP  38463  trficl  38487  dfrcl2  38492  relexpss1d  38523  trclrelexplem  38529  brtrclfv2  38545  dfrtrcl3  38551  heeq12  38596  sscon34b  38843  ntrk2imkb  38861  clsk3nimkb  38864  clsk1independent  38870  isotone1  38872  isotone2  38873  ntrclsss  38887  ntrclsiso  38891  ntrclsk2  38892  ntrclsk3  38894  nzss  39042  iunincfi  39793  fourierdlem89  40929  fourierdlem90  40930  fourierdlem91  40931  meaiuninclem  41214  meaiunincf  41217  meaiuninc3v  41218  meaiuninc3  41219  meaiininclem  41220  meaiininc  41221  caragenss  41238  carageniuncllem1  41255  ovnsslelem  41294  hoidmvle  41334  ovnhoilem2  41336  hoiqssbl  41359  ovolval5lem2  41387  ovolval5lem3  41388  vonioolem2  41415  vonicclem2  41418  uspgrsprf  42282  scmsuppss  42681
  Copyright terms: Public domain W3C validator