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

Theorem sseq12d 3667
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 3665 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
3 sseq12d.2 . . 3 (𝜑𝐶 = 𝐷)
43sseq2d 3666 . 2 (𝜑 → (𝐵𝐶𝐵𝐷))
52, 4bitrd 268 1 (𝜑 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  3sstr3d  3680  3sstr4d  3681  ssdifeq0  4084  relcnvtr  5693  knatar  6647  suppfnss  7365  funsssuppss  7366  smogt  7509  oawordri  7675  omwordi  7696  omwordri  7697  oewordi  7716  oewordri  7717  oeworde  7718  nnawordi  7746  nnmwordi  7760  nnmwordri  7761  sbthlem2  8112  sbth  8121  marypha2lem3  8384  hartogslem1  8488  inf3lem1  8563  tcrank  8785  alephle  8949  cfsmolem  9130  isfin3ds  9189  fin23lem17  9198  fin23lem39  9210  isf32lem1  9213  isf32lem2  9214  isf32lem11  9223  isf33lem  9226  isf34lem7  9239  isf34lem6  9240  fin1a2lem13  9272  itunitc1  9280  dominf  9305  dcomex  9307  axdc2lem  9308  dominfac  9433  fpwwe2cbv  9490  fpwwe2lem2  9492  fpwwecbv  9504  fpwwelem  9505  canthwelem  9510  canthwe  9511  wunex2  9598  swrdval  13462  trcleq2lem  13776  dfrtrcl2  13846  vdwpc  15731  vdwlem1  15732  vdwlem6  15737  vdwlem7  15738  vdwlem8  15739  isstruct2  15914  ressval  15974  mreexexlemd  16351  isacs1i  16365  isssc  16527  ssc2  16529  fullfunc  16613  fthfunc  16614  isps  17249  istsr  17264  isdir  17279  gsumvalx  17317  efgi2  18184  dmdprd  18443  dprdss  18474  dmdprdpr  18494  scmatdmat  20369  basis1  20802  baspartn  20806  eltg  20809  cncls  21126  ispnrm  21191  1stcfb  21296  2ndcctbss  21306  1stcelcls  21312  subislly  21332  kgenidm  21398  ptpjpre1  21422  txcmplem2  21493  flimval  21814  flimcf  21833  fclscf  21876  metss  22360  isngp  22447  iscph  23016  equivcau  23144  caubl  23152  caublcls  23153  ovoliunlem3  23318  volsuplem  23369  volsup  23370  dyaddisj  23410  itg1climres  23526  isausgr  26104  issubgr  26208  subgrprop3  26213  cusgrfilem1  26407  wkslem1  26559  wkslem2  26560  iswlk  26562  wlkres  26623  redwlk  26625  wlkp1lem8  26633  wlkdlem2  26636  crctcshwlkn0lem4  26761  crctcshwlkn0lem5  26762  crctcshwlkn0lem6  26763  2wlkdlem10  26900  3wlkdlem10  27147  eupthseg  27184  issh  28193  isch  28207  hsupss  28328  shslej  28367  shlub  28401  ledi  28527  pjoi0  28704  mdbr4  29285  dmdbr4  29293  dmdi4  29294  dmdbr5  29295  mdslle1i  29304  mdslle2i  29305  mdslmd1lem1  29312  mdslmd1lem2  29313  mdslmd1lem3  29314  mdslmd1lem4  29315  mdslmd1i  29316  sumdmdlem2  29406  resvval  29955  zhmnrg  30139  ispisys  30343  cvmliftlem3  31395  ismfs  31572  poimirlem32  33571  volsupnfl  33584  elrefrels2  34407  refreleq  34410  elcnvrefrels2  34420  dfsymrels2  34431  dfsymrel2  34435  elsymrels2  34439  symreleq  34444  elrefsymrels2  34453  lssatle  34620  pmaple  35365  2polcon4bN  35522  ispautN  35703  diaord  36653  dibord  36765  dihord6apre  36862  dihord3  36863  dihord4  36864  dihcnvord  36880  dvh4dimlem  37049  islpolN  37089  mapdordlem2  37243  mapdcnvordN  37264  mapdindp  37277  hdmaplkr  37522  ismrcd1  37578  ismrcd2  37579  ismrc  37581  incssnn0  37591  diophrw  37639  hbtlem5  38015  hbt  38017  rclexi  38239  rtrclex  38241  trclubgNEW  38242  rtrclexi  38245  cnvrcl0  38249  cnvtrcl0  38250  dfrtrcl5  38253  trcleq2lemRP  38254  trficl  38278  dfrcl2  38283  relexpss1d  38314  trclrelexplem  38320  brtrclfv2  38336  dfrtrcl3  38342  heeq12  38387  sscon34b  38634  ntrk2imkb  38652  clsk3nimkb  38655  clsk1independent  38661  isotone1  38663  isotone2  38664  ntrclsss  38678  ntrclsiso  38682  ntrclsk2  38683  ntrclsk3  38685  nzss  38833  iunincfi  39586  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  meaiuninclem  41015  meaiunincf  41018  meaiuninc3v  41019  meaiuninc3  41020  meaiininclem  41021  meaiininc  41022  caragenss  41039  carageniuncllem1  41056  ovnsslelem  41095  hoidmvle  41135  ovnhoilem2  41137  hoiqssbl  41160  ovolval5lem2  41188  ovolval5lem3  41189  vonioolem2  41216  vonicclem2  41219  uspgrsprf  42079  scmsuppss  42478
  Copyright terms: Public domain W3C validator