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

Theorem eqsstrd 3843
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 3836 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mpbird 248 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wss 3776
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 2791
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 2800  df-cleq 2806  df-clel 2809  df-in 3783  df-ss 3790
This theorem is referenced by:  eqsstr3d  3844  syl6eqss  3859  fpr2g  6703  tfisi  7291  suppssof1  7566  suppss2  7567  onfununi  7677  oawordeulem  7874  oeeui  7922  nnawordex  7957  oaabslem  7963  oaabs2  7965  omabslem  7966  omabs  7967  pw2f1olem  8306  fodomr  8353  fival  8560  dffi3  8579  ordtypelem7  8671  ordtypelem8  8672  wemapso2lem  8699  cantnflt2  8820  cantnflem1  8836  tcss  8870  tcel  8871  r1val1  8899  rankuni2b  8966  tcrank  8997  cardonle  9069  harval2  9109  carduniima  9205  ackbij2  9353  cfub  9359  cflecard  9363  cfflb  9369  isf32lem8  9470  itunitc1  9530  ttukeylem7  9625  fpwwe2lem9  9748  wuncss  9855  wuncval2  9857  grur1a  9929  trclfvub  13974  cotrtrclfv  13979  relexpfld  14015  rtrclreclem4  14027  limsupgre  14438  isercolllem3  14623  4sqlem19  15887  vdwlem1  15905  vdwlem12  15916  ramub1lem1  15950  setsstruct2  16110  setsstructOLD  16113  ressress  16153  imasaddfnlem  16396  imasaddflem  16398  imasvscafn  16405  imasvscaf  16407  imasless  16408  isohom  16643  ressffth  16805  acsfiindd  17385  acsmap2d  17387  dirref  17443  mrcmndind  17574  f1omvdco2  18072  pmtrfrn  18082  symgsssg  18091  symggen  18094  psgnunilem1  18117  sylow2alem2  18237  lsmssv  18262  lsmidm  18281  gsumzres  18514  dprdlub  18630  dprdf1  18637  dprdsn  18640  dprdcntz2  18642  dprd2dlem1  18645  dprd2da  18646  dmdprdsplit2lem  18649  ablfac1eu  18677  drnglpir  19465  issubassa2  19557  evlslem4  19719  evlseu  19727  znleval  20113  evpmss  20142  frlmsplit2  20326  f1lindf  20375  lpsscls  21163  tgrest  21181  resttopon  21183  rest0  21191  restfpw  21201  ordtrest  21224  ordtrest2  21226  lmcnp  21326  tgcmp  21422  uncmp  21424  hauscmplem  21427  1stcfb  21466  2ndcdisj  21477  dissnref  21549  kgencmp  21566  xkouni  21620  prdstopn  21649  txtube  21661  txcmplem2  21663  xkoptsub  21675  xkopt  21676  xkococnlem  21680  qtoprest  21738  imastopn  21741  kqdisj  21753  reghmph  21814  nrmhmph  21815  fbssfi  21858  trfilss  21910  trfg  21912  elfm3  21971  alexsubALTlem3  22070  alexsubALT  22072  cnextf  22087  cnextcn  22088  clsnsg  22130  tgpconncompeqg  22132  qustgphaus  22143  trust  22250  ustuqtop3  22264  neipcfilu  22317  metequiv2  22532  prdsxmslem2  22551  metustfbas  22579  icccmplem1  22842  metdstri  22871  pi1addf  23063  pi1addval  23064  caubl  23323  caublcls  23324  relcmpcmet  23332  minveclem4  23421  hlhil  23432  ovolficcss  23456  uniioombllem3a  23571  uniioombllem3  23572  dyadss  23581  opnmbllem  23588  i1fima2  23666  limcfval  23856  dvfval  23881  dvnres  23914  dvivth  23993  lhop  23999  taylf  24335  xrlimcnp  24915  jensen  24935  ppisval  25050  chtlepsi  25151  chpub  25165  iscgrglt  25629  chssoc  28689  mdsl0  29503  mdexchi  29528  atcvat3i  29589  dmdbr5ati  29615  funimass4f  29770  xrofsup  29866  locfinreflem  30238  cmpcref  30248  cnvordtrestixx  30290  ordtrestNEW  30298  ordtrest2NEW  30300  pnfneige0  30328  sigagenss  30543  imambfm  30655  dya2iocress  30667  dya2icoseg  30670  dya2iocucvr  30677  ballotlemro  30915  ftc2re  31007  bnj1097  31377  bnj1452  31448  cvmlift3lem6  31634  msubrn  31754  mclsssv  31789  mclsind  31795  trpredmintr  32056  noextend  32145  nosupbday  32177  scutun12  32243  scutbdaybnd  32247  scutbdaylt  32248  liness  32578  neibastop2lem  32681  opnmbllem0  33760  mblfinlem2  33762  isbndx  33894  isbnd2  33895  ssbnd  33900  heiborlem3  33925  igenmin  34176  lsatlss  34778  lsmsat  34790  lsatfixedN  34791  lssats  34794  lpssat  34795  lssatle  34797  lssat  34798  lsatcvat3  34834  paddssat  35596  paddasslem17  35618  pmodlem2  35629  hlmod1i  35638  pl42lem4N  35764  diassdvaN  36842  dia2dimlem10  36855  cdlemn4a  36981  cdlemn5pre  36982  dihord5apre  37044  lclkrlem2e  37293  lclkrlem2p  37304  lclkrlem2v  37310  lclkrslem2  37320  lclkrs  37321  lcfrlem25  37349  lcfrlem35  37359  mapdval2N  37412  mapdpglem8  37461  mapdpglem13  37466  baerlem3lem2  37492  mapdindp2  37503  hdmap11lem2  37624  elrfi  37760  isnacs3  37776  mzpf  37802  mzpindd  37812  diophrw  37825  eldiophss  37841  rmxyelqirr  37977  pw2f1ocnv  38106  aomclem6  38131  hbt  38202  rgspnmin  38243  cnvssb  38393  trclubgNEW  38426  dfrcl2  38467  fvmptiunrelexplb0da  38478  relexp0a  38509  cotrcltrcl  38518  trclimalb2  38519  cotrclrcl  38535  isotone2  38848  k0004ss1  38950  fnresdmss  39838  mptelpm  39847  founiiun0  39867  ssnnf1octb  39872  uzfissfz  40023  iuneqfzuzlem  40031  icccncfext  40581  dvnprodlem1  40642  dvnprodlem2  40643  dvnprodlem3  40644  fourierdlem41  40845  fourierdlem70  40873  fourierdlem71  40874  fourierdlem80  40883  fourierdlem113  40916  rrxbasefi  40983  ioorrnopnlem  41004  ioorrnopnxrlem  41006  salgenss  41034  dfsalgen2  41039  subsaliuncllem  41055  iundjiun  41157  meadjiunlem  41162  meaiunlelem  41165  meaiuninclem  41177  meaiininclem  41183  omeunle  41213  carageniuncllem2  41219  caratheodorylem1  41223  caratheodorylem2  41224  hoissre  41241  ovnsubaddlem1  41267  hoidmvlelem3  41294  ovnhoilem1  41298  ovnhoilem2  41299  ovnhoi  41300  ovncvr2  41308  voncmpl  41318  hspmbllem2  41324  hspmbl  41326  opnvonmbllem1  41329  vonmblss  41337  ovnsubadd2lem  41342  vonioolem2  41378  preimageiingt  41413  preimaleiinlt  41414  issmfd  41427  issmfdf  41429  sssmf  41430  cnfsmf  41432  issmfled  41449  issmfgtd  41452  smfadd  41456  smfrec  41479  smfmul  41485  smfmulc1  41486  smfpimbor1lem2  41489  smfsuplem1  41500  smflimsuplem1  41509  smflimsuplem7  41515  sprssspr  42300  linc1  42783
  Copyright terms: Public domain W3C validator