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

Theorem sseqtr4i 3846
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.)
Hypotheses
Ref Expression
sseqtr4.1 𝐴𝐵
sseqtr4.2 𝐶 = 𝐵
Assertion
Ref Expression
sseqtr4i 𝐴𝐶

Proof of Theorem sseqtr4i
StepHypRef Expression
1 sseqtr4.1 . 2 𝐴𝐵
2 sseqtr4.2 . . 3 𝐶 = 𝐵
32eqcomi 2826 . 2 𝐵 = 𝐶
41, 3sseqtri 3845 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637  wss 3780
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 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2795
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 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-in 3787  df-ss 3794
This theorem is referenced by:  eqimss2i  3868  difsssymdif  4064  snsspr1  4546  snsspr2  4547  snsstp1  4548  snsstp2  4549  snsstp3  4550  unissint  4704  iunxdif2  4771  pwpwssunieq  4818  intabs  5030  opabssxp  5408  dmresi  5682  cnvimass  5708  ssrnres  5796  sofld  5805  cnvcnv  5810  cnvcnvOLD  5811  cnvssrndm  5884  sssucid  6027  fvclss  6733  dmmpt2ssx  7477  suppun  7558  wfrlem14  7673  tfrlem11  7729  oawordeulem  7880  mapex  8107  trcl  8860  djuunxp  9039  dfac3  9236  cfsuc  9373  fin23lem11  9433  domtriomlem  9558  ttukeylem1  9625  ttukeylem7  9631  brdom7disj  9647  brdom6disj  9648  fingch  9739  fpwwe2lem13  9758  canthp1lem2  9769  wunex2  9854  wunex3  9857  ressxr  10377  ltrelxr  10393  nnssnn0  11581  un0addcl  11611  un0mulcl  11612  nn0ssxnn0  11651  fzssnn  12627  caubnd  14340  isumclim3  14732  iprodclim3  14970  bpoly4  15029  fprodefsum  15064  znnen  15180  isprm3  15633  phimullem  15720  vdwnnlem1  15935  isstruct2  16097  2strbas  16214  2strop  16215  2strbas1  16217  rngbase  16231  rngplusg  16232  rngmulr  16233  srngbase  16239  srngplusg  16240  srngmulr  16241  srnginvl  16242  lmodbase  16248  lmodplusg  16249  lmodsca  16250  lmodvsca  16251  ipsbase  16255  ipsaddg  16256  ipsmulr  16257  ipssca  16258  ipsvsca  16259  ipsip  16260  phlbase  16265  phlplusg  16266  phlsca  16267  phlvsca  16268  phlip  16269  topgrpbas  16273  topgrpplusg  16274  topgrptset  16275  otpsbas  16280  otpstset  16281  otpsle  16282  odrngbas  16291  odrngplusg  16292  odrngmulr  16293  odrngtset  16294  odrngle  16295  odrngds  16296  homarw  16919  ipoval  17378  ipolerval  17380  cycsubg  17843  eqgfval  17863  gsumval3  18528  islbs3  19383  cnfldbas  19977  cnfldadd  19978  cnfldmul  19979  cnfldcj  19980  cnfldtset  19981  cnfldle  19982  cnfldds  19983  cnfldunif  19984  basdif0  20991  iscldtop  21133  iocpnfordt  21253  icomnfordt  21254  iooordt  21255  cnrest2  21324  cmpcov2  21427  fiuncmp  21441  bwth  21447  indisconn  21455  locfincmp  21563  xkococnlem  21696  hmphdis  21833  uzrest  21934  ufildr  21968  fin1aufil  21969  eltsms  22169  ustval  22239  qtopbaslem  22795  tgqioo  22836  re2ndc  22837  xrhmeo  22978  bndth  22990  pi1xfrcnvlem  23088  ovolficcss  23472  nulmbl2  23539  uniiccdif  23581  opnmbllem  23604  opnmblALT  23606  mbfimaopnlem  23658  i1fima  23681  i1fima2  23682  i1fd  23684  c1liplem1  23995  deg1n0ima  24085  efcvx  24439  dvrelog  24619  dvloglem  24630  logf1o2  24632  dvlog  24633  ressatans  24897  wilthlem3  25032  trkgbas  25580  trkgdist  25581  trkgitv  25582  ex-ss  27637  ajfval  28014  ipasslem8  28042  hlimcaui  28443  shsspwh  28453  hhssabloi  28469  hhssnv  28471  hhshsslem1  28474  shunssji  28578  sshhococi  28755  pjoml6i  28798  osumcori  28852  mayete3i  28937  mayetes3i  28938  imaelshi  29267  pjclem1  29404  pjci  29409  mdcompli  29638  dmdcompli  29639  xppreima  29798  gsummpt2co  30127  circtopn  30251  esumpcvgval  30487  esumcvg  30495  ldgenpisyslem3  30575  elmbfmvol2  30676  sxbrsigalem0  30680  eulerpartlemsv3  30770  ballotlem7  30944  rpsqrtcn  31018  bnj931  31185  bnj1137  31407  subfacp1lem2a  31506  subfacp1lem2b  31507  erdszelem2  31518  kur14lem7  31538  kur14lem9  31540  dfon2lem2  32030  bj-snglsstag  33297  bj-2upln1upl  33340  bj-0int  33384  bj-ccssccbar  33439  bj-ccinftyssccbar  33440  icoreelrn  33543  finxpreclem3  33564  imadifss  33715  poimirlem4  33744  poimirlem26  33766  poimirlem27  33767  opnmbllem0  33776  mblfinlem3  33779  mblfinlem4  33780  ismblfin  33781  volsupnfl  33785  sdclem2  33867  heibor1lem  33937  inxpssres  34410  dicval  36974  dvhdimlem  37242  ismrc  37783  mapfzcons1cl  37800  2rexfrabdioph  37879  3rexfrabdioph  37880  4rexfrabdioph  37881  6rexfrabdioph  37882  7rexfrabdioph  37883  rabdiophlem2  37885  jm2.27dlem5  38098  algbase  38266  algaddg  38267  algmulr  38268  algsca  38269  algvsca  38270  intimass2  38464  comptiunov2i  38515  relexp0a  38525  lhe4.4ex1a  39045  iocnct  40264  iccnct  40265  dvcosre  40623  fourierdlem46  40865  fourierdlem57  40876  fourierdlem58  40877  fourierdlem62  40881  fourierdlem102  40921  fourierdlem103  40922  fourierdlem104  40923  fourierdlem114  40933  sge0split  41122  sge0uzfsumgt  41157  hoiprodp1  41301  hoidmvlelem1  41308  hoidmvlelem2  41309  hoidmvlelem3  41310  sbgoldbo  42267  dmmpt2ssx2  42700  aacllem  43135
  Copyright terms: Public domain W3C validator