Theorem eqsstrd 3964

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 3957	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
4	1, 3	mpbird 257	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-in 3899  df-ss 3909

This theorem is referenced by:  eqsstrrd  3965  eqsstrdi  3980  fpr2g  7119  tfisi  7737  suppssof1  8046  suppss2  8047  onfununi  8203  oawordeulem  8416  oeeui  8464  nnawordex  8499  oaabslem  8508  oaabs2  8510  omabslem  8511  omabs  8512  pw2f1olem  8901  fodomr  8953  fival  9215  dffi3  9234  ordtypelem7  9327  ordtypelem8  9328  wemapso2lem  9355  cantnflt2  9475  cantnflem1  9491  tcss  9546  tcel  9547  r1val1  9588  rankuni2b  9655  tcrank  9686  cardonle  9759  harval2  9799  ackbij2  10045  cfub  10051  cflecard  10055  cfflb  10061  isf32lem8  10162  itunitc1  10222  ttukeylem7  10317  fpwwe2lem8  10440  wuncss  10547  wuncval2  10549  grur1a  10621  trclfvub  14763  cotrtrclfv  14768  relexpfld  14805  rtrclreclem4  14817  limsupgre  15235  isercolllem3  15423  4sqlem19  16709  vdwlem1  16727  vdwlem12  16738  ramub1lem1  16772  setsstruct2  16920  ressress  17003  imasaddfnlem  17284  imasaddflem  17286  imasvscafn  17293  imasvscaf  17295  imasless  17296  isohom  17533  ressffth  17699  acsfiindd  18316  acsmap2d  18318  dirref  18364  mndind  18511  f1omvdco2  19101  pmtrfrn  19111  symgsssg  19120  symggen  19123  psgnunilem1  19146  sylow2alem2  19268  lsmssv  19293  smndlsmidm  19306  lsmidmOLD  19314  gsumzres  19555  dprdlub  19674  dprdf1  19681  dprdsn  19684  dprdcntz2  19686  dprd2dlem1  19689  dprd2da  19690  dmdprdsplit2lem  19693  ablfac1eu  19721  drnglpir  20569  znleval  20807  evpmss  20836  frlmsplit2  21025  f1lindf  21074  issubassa2  21141  mplsubglem  21250  evlslem4  21329  evlseu  21338  mhpaddcl  21386  mhpinvcl  21387  lpsscls  22337  tgrest  22355  resttopon  22357  rest0  22365  restfpw  22375  ordtrest  22398  ordtrest2  22400  lmcnp  22500  tgcmp  22597  uncmp  22599  hauscmplem  22602  1stcfb  22641  2ndcdisj  22652  dissnref  22724  kgencmp  22741  xkouni  22795  prdstopn  22824  txtube  22836  txcmplem2  22838  xkoptsub  22850  xkopt  22851  xkococnlem  22855  qtoprest  22913  imastopn  22916  kqdisj  22928  reghmph  22989  nrmhmph  22990  fbssfi  23033  trfilss  23085  trfg  23087  elfm3  23146  alexsubALTlem3  23245  alexsubALT  23247  cnextf  23262  cnextcn  23263  clsnsg  23306  tgpconncompeqg  23308  qustgphaus  23319  trust  23426  ustuqtop3  23440  neipcfilu  23493  metequiv2  23711  prdsxmslem2  23730  metustfbas  23758  icccmplem1  24030  metdstri  24059  pi1addf  24255  pi1addval  24256  caubl  24517  caublcls  24518  relcmpcmet  24527  minveclem4  24641  hlhil  24652  ovolficcss  24678  uniioombllem3a  24793  uniioombllem3  24794  dyadss  24803  opnmbllem  24810  i1fima2  24888  limcfval  25081  dvfval  25106  dvnres  25140  dvivth  25219  lhop  25225  taylf  25565  xrlimcnp  26163  jensen  26183  ppisval  26298  chtlepsi  26399  chpub  26413  iscgrglt  26920  chssoc  29903  mdsl0  30717  mdexchi  30742  atcvat3i  30803  dmdbr5ati  30829  funimass4f  31017  xrofsup  31135  swrdrn2  31271  gsumpart  31360  pmtrcnel  31403  tocycfvres1  31422  tocycfvres2  31423  cycpmco2lem6  31443  cycpmconjvlem  31453  cycpmconjslem2  31467  nsgmgc  31642  idlsrgmulrss1  31701  idlsrgmulrss2  31702  fedgmullem1  31755  fedgmullem2  31756  ist0cld  31828  locfinreflem  31835  cmpcref  31845  zarcls0  31863  zarclsiin  31866  zarcmplem  31876  cnvordtrestixx  31908  ordtrestNEW  31916  ordtrest2NEW  31918  pnfneige0  31946  sigagenss  32162  imambfm  32274  dya2iocress  32286  dya2icoseg  32289  dya2iocucvr  32296  ballotlemro  32534  ftc2re  32623  bnj1097  33006  bnj1452  33077  cvmlift3lem6  33331  msubrn  33536  mclsssv  33571  mclsind  33577  noextend  33914  nosupbday  33953  noinfbday  33968  scutun12  34049  scutbdaybnd  34054  scutbdaybnd2  34055  scutbdaylt  34057  cofcut1  34135  cofcutr  34137  liness  34492  neibastop2lem  34594  opnmbllem0  35857  mblfinlem2  35859  isbndx  35984  isbnd2  35985  ssbnd  35990  heiborlem3  36015  igenmin  36266  lsatlss  37052  lsmsat  37064  lsatfixedN  37065  lssats  37068  lpssat  37069  lssatle  37071  lssat  37072  lsatcvat3  37108  paddssat  37870  paddasslem17  37892  pmodlem2  37903  hlmod1i  37912  pl42lem4N  38038  diassdvaN  39116  dia2dimlem10  39129  cdlemn4a  39255  cdlemn5pre  39256  dihord5apre  39318  lclkrlem2e  39567  lclkrlem2p  39578  lclkrlem2v  39584  lclkrslem2  39594  lclkrs  39595  lcfrlem25  39623  lcfrlem35  39633  mapdval2N  39686  mapdpglem8  39735  mapdpglem13  39740  baerlem3lem2  39766  mapdindp2  39777  hdmap11lem2  39898  elrfi  40553  isnacs3  40569  mzpf  40595  mzpindd  40605  diophrw  40618  eldiophss  40633  rmxyelqirrOLD  40770  pw2f1ocnv  40897  aomclem6  40922  hbt  40993  rgspnmin  41034  minregex  41179  cnvssb  41232  trclubgNEW  41264  dfrcl2  41320  fvmptiunrelexplb0da  41331  relexp0a  41362  cotrcltrcl  41371  trclimalb2  41372  cotrclrcl  41388  isotone2  41697  k0004ss1  41799  fnresdmss  42748  mptelpm  42756  ssnnf1octb  42777  uzfissfz  42913  iuneqfzuzlem  42921  xlimliminflimsup  43452  icccncfext  43477  dvnprodlem1  43536  dvnprodlem2  43537  dvnprodlem3  43538  fourierdlem41  43738  fourierdlem70  43766  fourierdlem71  43767  fourierdlem80  43776  fourierdlem113  43809  ioorrnopnlem  43894  ioorrnopnxrlem  43896  salgenss  43924  dfsalgen2  43929  subsaliuncllem  43945  iundjiun  44048  meadjiunlem  44053  meaiunlelem  44056  meaiuninclem  44068  meaiininclem  44074  omeunle  44104  carageniuncllem2  44110  caratheodorylem1  44114  caratheodorylem2  44115  hoissre  44132  ovnsubaddlem1  44158  hoidmvlelem3  44185  ovnhoilem1  44189  ovnhoilem2  44190  ovnhoi  44191  ovncvr2  44199  voncmpl  44209  hspmbllem2  44215  hspmbl  44217  opnvonmbllem1  44220  vonmblss  44228  ovnsubadd2lem  44233  vonioolem2  44269  preimageiingt  44308  preimaleiinlt  44309  issmfd  44323  issmfdf  44325  sssmf  44326  cnfsmf  44328  issmfled  44345  issmfgtd  44349  smfadd  44353  smfrec  44377  smfmul  44383  smfmulc1  44384  smfpimbor1lem2  44387  smfsuplem1  44398  smflimsuplem1  44407  smflimsuplem7  44413  sprssspr  44991  linc1  45824