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

Theorem eqsstrd 3602
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
eqsstrd.1 (𝜑𝐴 = 𝐵)
eqsstrd.2 (𝜑𝐵𝐶)
Assertion
Ref Expression
eqsstrd (𝜑𝐴𝐶)

Proof of Theorem eqsstrd
StepHypRef Expression
1 eqsstrd.2 . 2 (𝜑𝐵𝐶)
2 eqsstrd.1 . . 3 (𝜑𝐴 = 𝐵)
32sseq1d 3595 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mpbird 246 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554
This theorem is referenced by:  eqsstr3d  3603  syl6eqss  3618  fpr2g  6380  tfisi  6950  suppssof1  7215  suppss2  7216  onfununi  7325  oawordeulem  7521  oeeui  7569  nnawordex  7604  oaabslem  7610  oaabs2  7612  omabslem  7613  omabs  7614  pw2f1olem  7949  fodomr  7996  fival  8201  dffi3  8220  ordtypelem7  8312  ordtypelem8  8313  wemapso2lem  8340  cantnflt2  8453  cantnflem1  8469  tcss  8503  tcel  8504  r1val1  8532  rankuni2b  8599  tcrank  8630  cardonle  8666  harval2  8706  carduniima  8802  ackbij2  8948  cfub  8954  cflecard  8958  cfflb  8964  isf32lem8  9065  itunitc1  9125  ttukeylem7  9220  fpwwe2lem9  9339  wuncss  9446  wuncval2  9448  grur1a  9520  trclfvub  13596  cotrtrclfv  13601  relexpfld  13637  rtrclreclem4  13649  limsupgre  14060  isercolllem3  14245  4sqlem19  15505  vdwlem1  15523  vdwlem12  15534  ramub1lem1  15568  setsstruct  15727  ressress  15765  imasaddfnlem  16011  imasaddflem  16013  imasvscafn  16020  imasvscaf  16022  imasless  16023  isohom  16259  ressffth  16421  acsfiindd  17000  acsmap2d  17002  dirref  17058  mrcmndind  17189  f1omvdco2  17691  pmtrfrn  17701  symgsssg  17710  symggen  17713  psgnunilem1  17736  sylow2alem2  17856  lsmssv  17881  lsmidm  17900  gsumzres  18133  dprdlub  18248  dprdf1  18255  dprdsn  18258  dprdcntz2  18260  dprd2dlem1  18263  dprd2da  18264  dmdprdsplit2lem  18267  ablfac1eu  18295  drnglpir  19074  issubassa2  19166  evlslem4  19329  evlseu  19337  znleval  19722  evpmss  19751  frlmsplit2  19931  f1lindf  19980  lpsscls  20755  tgrest  20773  resttopon  20775  rest0  20783  restfpw  20793  ordtrest  20816  ordtrest2  20818  lmcnp  20918  tgcmp  21014  uncmp  21016  hauscmplem  21019  1stcfb  21058  2ndcdisj  21069  dissnref  21141  kgencmp  21158  xkouni  21212  prdstopn  21241  txtube  21253  txcmplem2  21255  xkoptsub  21267  xkopt  21268  xkococnlem  21272  qtoprest  21330  imastopn  21333  kqdisj  21345  reghmph  21406  nrmhmph  21407  fbssfi  21451  trfilss  21503  trfg  21505  elfm3  21564  alexsubALTlem3  21663  alexsubALT  21665  cnextf  21680  cnextcn  21681  clsnsg  21723  tgpconcompeqg  21725  qustgphaus  21736  trust  21843  ustuqtop3  21857  neipcfilu  21910  metequiv2  22125  prdsxmslem2  22144  metustfbas  22172  icccmplem1  22433  metdstri  22462  pi1addf  22655  pi1addval  22656  caubl  22914  caublcls  22915  relcmpcmet  22923  minveclem4  23011  hlhil  23022  ovolficcss  23045  uniioombllem3a  23158  uniioombllem3  23159  dyadss  23168  opnmbllem  23175  i1fima2  23252  limcfval  23442  dvfval  23467  dvnres  23500  dvivth  23577  lhop  23583  taylf  23919  xrlimcnp  24495  jensen  24515  ppisval  24630  chtlepsi  24731  chpub  24745  iscgrglt  25209  uhgredgn0  25802  upgredgss  25806  umgredgss  25807  edgss  25881  chssoc  27739  mdsl0  28553  mdexchi  28578  atcvat3i  28639  dmdbr5ati  28665  funimass4f  28818  xrofsup  28923  locfinreflem  29235  cmpcref  29245  cnvordtrestixx  29287  ordtrestNEW  29295  ordtrest2NEW  29297  pnfneige0  29325  sigagenss  29539  imambfm  29651  dya2iocress  29663  dya2icoseg  29666  dya2iocucvr  29673  ballotlemro  29911  bnj1097  30303  bnj1452  30374  cvmlift3lem6  30560  msubrn  30680  mclsssv  30715  mclsind  30721  trpredmintr  30975  nobndlem8  31098  liness  31422  neibastop2lem  31525  opnmbllem0  32615  mblfinlem2  32617  isbndx  32751  isbnd2  32752  ssbnd  32757  heiborlem3  32782  igenmin  33033  lsatlss  33301  lsmsat  33313  lsatfixedN  33314  lssats  33317  lpssat  33318  lssatle  33320  lssat  33321  lsatcvat3  33357  paddssat  34118  paddasslem17  34140  pmodlem2  34151  hlmod1i  34160  pl42lem4N  34286  diassdvaN  35367  dia2dimlem10  35380  cdlemn4a  35506  cdlemn5pre  35507  dihord5apre  35569  lclkrlem2e  35818  lclkrlem2p  35829  lclkrlem2v  35835  lclkrslem2  35845  lclkrs  35846  lcfrlem25  35874  lcfrlem35  35884  mapdval2N  35937  mapdpglem8  35986  mapdpglem13  35991  baerlem3lem2  36017  mapdindp2  36028  hdmap11lem2  36152  elrfi  36275  isnacs3  36291  mzpf  36317  mzpindd  36327  diophrw  36340  eldiophss  36356  rmxyelqirr  36493  pw2f1ocnv  36622  aomclem6  36647  hbt  36719  rgspnmin  36760  cnvssb  36911  trclubgNEW  36944  dfrcl2  36985  fvmptiunrelexplb0da  36996  relexp0a  37027  cotrcltrcl  37036  trclimalb2  37037  cotrclrcl  37053  isotone2  37367  k0004ss1  37469  fnresdmss  38342  mptelpm  38352  founiiun0  38372  ssnnf1octb  38377  uzfissfz  38483  iuneqfzuzlem  38491  icccncfext  38773  dvnprodlem1  38836  dvnprodlem2  38837  dvnprodlem3  38838  fourierdlem41  39041  fourierdlem70  39069  fourierdlem71  39070  fourierdlem80  39079  fourierdlem113  39112  rrxbasefi  39179  ioorrnopnlem  39200  ioorrnopnxrlem  39202  salgenss  39230  dfsalgen2  39235  subsaliuncllem  39251  iundjiun  39353  meadjiunlem  39358  meaiunlelem  39361  meaiuninclem  39373  meaiininclem  39376  omeunle  39406  carageniuncllem2  39412  caratheodorylem1  39416  caratheodorylem2  39417  hoissre  39434  ovnsubaddlem1  39460  hoidmvlelem3  39487  ovnhoilem1  39491  ovnhoilem2  39492  ovnhoi  39493  ovncvr2  39501  voncmpl  39511  hspmbllem2  39517  hspmbl  39519  opnvonmbllem1  39522  vonmblss  39530  ovnsubadd2lem  39535  vonioolem2  39572  preimageiingt  39607  preimaleiinlt  39608  issmfd  39621  issmfdf  39624  sssmf  39625  cnfsmf  39627  issmfled  39644  issmfgtd  39647  smfadd  39651  smfrec  39674  smfmul  39680  smfmulc1  39681  smfpimbor1lem2  39684  usgredgss  40390  linc1  42008
  Copyright terms: Public domain W3C validator