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

Theorem sseq12d 3997
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 3995 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
3 sseq12d.2 . . 3 (𝜑𝐶 = 𝐷)
43sseq2d 3996 . 2 (𝜑 → (𝐵𝐶𝐵𝐷))
52, 4bitrd 280 1 (𝜑 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-in 3940  df-ss 3949
This theorem is referenced by:  3sstr3d  4010  3sstr4d  4011  ssdifeq0  4428  relcnvtrg  6112  knatar  7099  suppfnss  7844  funsssuppss  7845  smogt  7993  oawordri  8165  omwordi  8186  omwordri  8187  oewordi  8206  oewordri  8207  oeworde  8208  nnawordi  8236  nnmwordi  8250  nnmwordri  8251  sbthlem2  8616  sbth  8625  marypha2lem3  8889  hartogslem1  8994  inf3lem1  9079  tcrank  9301  alephle  9502  cfsmolem  9680  isfin3ds  9739  fin23lem17  9748  fin23lem39  9760  isf32lem1  9763  isf32lem2  9764  isf32lem11  9773  isf33lem  9776  isf34lem7  9789  isf34lem6  9790  fin1a2lem13  9822  itunitc1  9830  dominf  9855  dcomex  9857  axdc2lem  9858  dominfac  9983  fpwwe2cbv  10040  fpwwe2lem2  10042  fpwwecbv  10054  fpwwelem  10055  canthwelem  10060  canthwe  10061  wunex2  10148  swrdval  13993  trcleq2lem  14339  dfrtrcl2  14409  vdwpc  16304  vdwlem1  16305  vdwlem6  16310  vdwlem7  16311  vdwlem8  16312  isstruct2  16481  ressval  16539  mreexexlemd  16903  isacs1i  16916  isssc  17078  ssc2  17080  fullfunc  17164  fthfunc  17165  isps  17800  istsr  17815  isdir  17830  gsumvalx  17874  efgi2  18780  dmdprd  19049  dprdss  19080  dmdprdpr  19100  mhpfval  20260  scmatdmat  21052  basis1  21486  baspartn  21490  eltg  21493  cncls  21810  ispnrm  21875  1stcfb  21981  2ndcctbss  21991  1stcelcls  21997  subislly  22017  kgenidm  22083  ptpjpre1  22107  txcmplem2  22178  flimval  22499  flimcf  22518  fclscf  22561  metss  23045  isngp  23132  iscph  23701  cphsscph  23781  equivcau  23830  caubl  23838  caublcls  23839  ovoliunlem3  24032  volsuplem  24083  volsup  24084  dyaddisj  24124  itg1climres  24242  isausgr  26876  issubgr  26980  subgrprop3  26985  cusgrfilem1  27164  wkslem1  27316  wkslem2  27317  iswlk  27319  wlkres  27379  redwlk  27381  wlkp1lem8  27389  wlkdlem2  27392  crctcshwlkn0lem4  27518  crctcshwlkn0lem5  27519  crctcshwlkn0lem6  27520  2wlkdlem10  27641  3wlkdlem10  27875  eupthseg  27912  issh  28912  isch  28926  hsupss  29045  shslej  29084  shlub  29118  ledi  29244  pjoi0  29421  mdbr4  30002  dmdbr4  30010  dmdi4  30011  dmdbr5  30012  mdslle1i  30021  mdslle2i  30022  mdslmd1lem1  30029  mdslmd1lem2  30030  mdslmd1lem3  30031  mdslmd1lem4  30032  mdslmd1i  30033  sumdmdlem2  30123  resvval  30827  zhmnrg  31107  ispisys  31310  pfxwlk  32267  cvmliftlem3  32431  ismfs  32693  rdgssun  34541  poimirlem32  34805  volsupnfl  34818  elrefrels2  35637  refreleq  35640  elcnvrefrels2  35650  dfsymrels2  35661  dfsymrel2  35665  elsymrels2  35669  symreleq  35674  elrefsymrels2  35685  dftrrels2  35691  dftrrel2  35693  eltrrels2  35695  trreleq  35698  eleqvrels2  35707  lssatle  36031  pmaple  36777  2polcon4bN  36934  ispautN  37115  diaord  38063  dibord  38175  dihord6apre  38272  dihord3  38273  dihord4  38274  dihcnvord  38290  dvh4dimlem  38459  islpolN  38499  mapdordlem2  38653  mapdcnvordN  38674  mapdindp  38687  hdmaplkr  38929  ismrcd1  39173  ismrcd2  39174  ismrc  39176  incssnn0  39186  diophrw  39234  hbtlem5  39606  hbt  39608  rclexi  39853  rtrclex  39855  trclubgNEW  39856  rtrclexi  39859  cnvrcl0  39863  cnvtrcl0  39864  dfrtrcl5  39867  trcleq2lemRP  39868  trficl  39892  dfrcl2  39897  relexpss1d  39928  trclrelexplem  39934  brtrclfv2  39950  dfrtrcl3  39956  heeq12  40000  sscon34b  40247  ntrk2imkb  40265  clsk3nimkb  40268  clsk1independent  40274  isotone1  40276  isotone2  40277  ntrclsss  40291  ntrclsiso  40295  ntrclsk2  40296  ntrclsk3  40298  scottabf  40453  ismnu  40474  nzss  40526  iunincfi  41237  fourierdlem89  42357  fourierdlem90  42358  fourierdlem91  42359  meaiuninclem  42639  meaiunincf  42642  meaiuninc3v  42643  meaiuninc3  42644  meaiininclem  42645  meaiininc  42646  caragenss  42663  carageniuncllem1  42680  ovnsslelem  42719  hoidmvle  42759  ovnhoilem2  42761  hoiqssbl  42784  ovolval5lem2  42812  ovolval5lem3  42813  vonioolem2  42840  vonicclem2  42843  uspgrsprf  43898  scmsuppss  44348
  Copyright terms: Public domain W3C validator