Theorem eqsstrd 3639

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

Step	Hyp	Ref	Expression
1		eqsstrd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
2		eqsstrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	sseq1d 3632	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
4	1, 3	mpbird 247	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1483   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  eqsstr3d  3640  syl6eqss  3655  fpr2g  6475  tfisi  7058  suppssof1  7328  suppss2  7329  onfununi  7438  oawordeulem  7634  oeeui  7682  nnawordex  7717  oaabslem  7723  oaabs2  7725  omabslem  7726  omabs  7727  pw2f1olem  8064  fodomr  8111  fival  8318  dffi3  8337  ordtypelem7  8429  ordtypelem8  8430  wemapso2lem  8457  cantnflt2  8570  cantnflem1  8586  tcss  8620  tcel  8621  r1val1  8649  rankuni2b  8716  tcrank  8747  cardonle  8783  harval2  8823  carduniima  8919  ackbij2  9065  cfub  9071  cflecard  9075  cfflb  9081  isf32lem8  9182  itunitc1  9242  ttukeylem7  9337  fpwwe2lem9  9460  wuncss  9567  wuncval2  9569  grur1a  9641  trclfvub  13748  cotrtrclfv  13753  relexpfld  13789  rtrclreclem4  13801  limsupgre  14212  isercolllem3  14397  4sqlem19  15667  vdwlem1  15685  vdwlem12  15696  ramub1lem1  15730  setsstruct2  15896  setsstructOLD  15899  ressress  15938  imasaddfnlem  16188  imasaddflem  16190  imasvscafn  16197  imasvscaf  16199  imasless  16200  isohom  16436  ressffth  16598  acsfiindd  17177  acsmap2d  17179  dirref  17235  mrcmndind  17366  f1omvdco2  17868  pmtrfrn  17878  symgsssg  17887  symggen  17890  psgnunilem1  17913  sylow2alem2  18033  lsmssv  18058  lsmidm  18077  gsumzres  18310  dprdlub  18425  dprdf1  18432  dprdsn  18435  dprdcntz2  18437  dprd2dlem1  18440  dprd2da  18441  dmdprdsplit2lem  18444  ablfac1eu  18472  drnglpir  19253  issubassa2  19345  evlslem4  19508  evlseu  19516  znleval  19903  evpmss  19932  frlmsplit2  20112  f1lindf  20161  lpsscls  20945  tgrest  20963  resttopon  20965  rest0  20973  restfpw  20983  ordtrest  21006  ordtrest2  21008  lmcnp  21108  tgcmp  21204  uncmp  21206  hauscmplem  21209  1stcfb  21248  2ndcdisj  21259  dissnref  21331  kgencmp  21348  xkouni  21402  prdstopn  21431  txtube  21443  txcmplem2  21445  xkoptsub  21457  xkopt  21458  xkococnlem  21462  qtoprest  21520  imastopn  21523  kqdisj  21535  reghmph  21596  nrmhmph  21597  fbssfi  21641  trfilss  21693  trfg  21695  elfm3  21754  alexsubALTlem3  21853  alexsubALT  21855  cnextf  21870  cnextcn  21871  clsnsg  21913  tgpconncompeqg  21915  qustgphaus  21926  trust  22033  ustuqtop3  22047  neipcfilu  22100  metequiv2  22315  prdsxmslem2  22334  metustfbas  22362  icccmplem1  22625  metdstri  22654  pi1addf  22847  pi1addval  22848  caubl  23106  caublcls  23107  relcmpcmet  23115  minveclem4  23203  hlhil  23214  ovolficcss  23238  uniioombllem3a  23352  uniioombllem3  23353  dyadss  23362  opnmbllem  23369  i1fima2  23446  limcfval  23636  dvfval  23661  dvnres  23694  dvivth  23773  lhop  23779  taylf  24115  xrlimcnp  24695  jensen  24715  ppisval  24830  chtlepsi  24931  chpub  24945  iscgrglt  25409  chssoc  28355  mdsl0  29169  mdexchi  29194  atcvat3i  29255  dmdbr5ati  29281  funimass4f  29437  xrofsup  29533  locfinreflem  29907  cmpcref  29917  cnvordtrestixx  29959  ordtrestNEW  29967  ordtrest2NEW  29969  pnfneige0  29997  sigagenss  30212  imambfm  30324  dya2iocress  30336  dya2icoseg  30339  dya2iocucvr  30346  ballotlemro  30584  ftc2re  30676  bnj1097  31049  bnj1452  31120  cvmlift3lem6  31306  msubrn  31426  mclsssv  31461  mclsind  31467  trpredmintr  31731  noextend  31819  nosupbday  31851  scutun12  31917  scutbdaybnd  31921  scutbdaylt  31922  liness  32252  neibastop2lem  32355  opnmbllem0  33445  mblfinlem2  33447  isbndx  33581  isbnd2  33582  ssbnd  33587  heiborlem3  33612  igenmin  33863  lsatlss  34283  lsmsat  34295  lsatfixedN  34296  lssats  34299  lpssat  34300  lssatle  34302  lssat  34303  lsatcvat3  34339  paddssat  35100  paddasslem17  35122  pmodlem2  35133  hlmod1i  35142  pl42lem4N  35268  diassdvaN  36349  dia2dimlem10  36362  cdlemn4a  36488  cdlemn5pre  36489  dihord5apre  36551  lclkrlem2e  36800  lclkrlem2p  36811  lclkrlem2v  36817  lclkrslem2  36827  lclkrs  36828  lcfrlem25  36856  lcfrlem35  36866  mapdval2N  36919  mapdpglem8  36968  mapdpglem13  36973  baerlem3lem2  36999  mapdindp2  37010  hdmap11lem2  37134  elrfi  37257  isnacs3  37273  mzpf  37299  mzpindd  37309  diophrw  37322  eldiophss  37338  rmxyelqirr  37475  pw2f1ocnv  37604  aomclem6  37629  hbt  37700  rgspnmin  37741  cnvssb  37892  trclubgNEW  37925  dfrcl2  37966  fvmptiunrelexplb0da  37977  relexp0a  38008  cotrcltrcl  38017  trclimalb2  38018  cotrclrcl  38034  isotone2  38347  k0004ss1  38449  fnresdmss  39348  mptelpm  39357  founiiun0  39377  ssnnf1octb  39382  uzfissfz  39542  iuneqfzuzlem  39550  icccncfext  40100  dvnprodlem1  40161  dvnprodlem2  40162  dvnprodlem3  40163  fourierdlem41  40365  fourierdlem70  40393  fourierdlem71  40394  fourierdlem80  40403  fourierdlem113  40436  rrxbasefi  40503  ioorrnopnlem  40524  ioorrnopnxrlem  40526  salgenss  40554  dfsalgen2  40559  subsaliuncllem  40575  iundjiun  40677  meadjiunlem  40682  meaiunlelem  40685  meaiuninclem  40697  meaiininclem  40700  omeunle  40730  carageniuncllem2  40736  caratheodorylem1  40740  caratheodorylem2  40741  hoissre  40758  ovnsubaddlem1  40784  hoidmvlelem3  40811  ovnhoilem1  40815  ovnhoilem2  40816  ovnhoi  40817  ovncvr2  40825  voncmpl  40835  hspmbllem2  40841  hspmbl  40843  opnvonmbllem1  40846  vonmblss  40854  ovnsubadd2lem  40859  vonioolem2  40895  preimageiingt  40930  preimaleiinlt  40931  issmfd  40944  issmfdf  40946  sssmf  40947  cnfsmf  40949  issmfled  40966  issmfgtd  40969  smfadd  40973  smfrec  40996  smfmul  41002  smfmulc1  41003  smfpimbor1lem2  41006  smfsuplem1  41017  smflimsuplem1  41026  smflimsuplem7  41032  sprssspr  41731  linc1  42214