Theorem eqsstrd 3926

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

Syntax hints:   → wi 4   = wceq 1522   ⊆ wss 3859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-in 3866  df-ss 3874

This theorem is referenced by:  eqsstrrd  3927  syl6eqss  3942  fpr2g  6840  tfisi  7429  suppssof1  7714  suppss2  7715  onfununi  7830  oawordeulem  8030  oeeui  8078  nnawordex  8113  oaabslem  8120  oaabs2  8122  omabslem  8123  omabs  8124  pw2f1olem  8468  fodomr  8515  fival  8722  dffi3  8741  ordtypelem7  8834  ordtypelem8  8835  wemapso2lem  8862  cantnflt2  8982  cantnflem1  8998  tcss  9032  tcel  9033  r1val1  9061  rankuni2b  9128  tcrank  9159  cardonle  9232  harval2  9272  ackbij2  9511  cfub  9517  cflecard  9521  cfflb  9527  isf32lem8  9628  itunitc1  9688  ttukeylem7  9783  fpwwe2lem9  9906  wuncss  10013  wuncval2  10015  grur1a  10087  trclfvub  14201  cotrtrclfv  14206  relexpfld  14242  rtrclreclem4  14254  limsupgre  14672  isercolllem3  14857  4sqlem19  16128  vdwlem1  16146  vdwlem12  16157  ramub1lem1  16191  setsstruct2  16350  ressress  16391  imasaddfnlem  16630  imasaddflem  16632  imasvscafn  16639  imasvscaf  16641  imasless  16642  isohom  16875  ressffth  17037  acsfiindd  17616  acsmap2d  17618  dirref  17674  mndind  17805  f1omvdco2  18307  pmtrfrn  18317  symgsssg  18326  symggen  18329  psgnunilem1  18352  sylow2alem2  18473  lsmssv  18498  lsmidm  18517  gsumzres  18750  dprdlub  18865  dprdf1  18872  dprdsn  18875  dprdcntz2  18877  dprd2dlem1  18880  dprd2da  18881  dmdprdsplit2lem  18884  ablfac1eu  18912  drnglpir  19715  issubassa2  19813  evlslem4  19975  evlseu  19983  mhpaddcl  20021  mhpinvcl  20022  znleval  20383  evpmss  20412  frlmsplit2  20599  f1lindf  20648  lpsscls  21433  tgrest  21451  resttopon  21453  rest0  21461  restfpw  21471  ordtrest  21494  ordtrest2  21496  lmcnp  21596  tgcmp  21693  uncmp  21695  hauscmplem  21698  1stcfb  21737  2ndcdisj  21748  dissnref  21820  kgencmp  21837  xkouni  21891  prdstopn  21920  txtube  21932  txcmplem2  21934  xkoptsub  21946  xkopt  21947  xkococnlem  21951  qtoprest  22009  imastopn  22012  kqdisj  22024  reghmph  22085  nrmhmph  22086  fbssfi  22129  trfilss  22181  trfg  22183  elfm3  22242  alexsubALTlem3  22341  alexsubALT  22343  cnextf  22358  cnextcn  22359  clsnsg  22401  tgpconncompeqg  22403  qustgphaus  22414  trust  22521  ustuqtop3  22535  neipcfilu  22588  metequiv2  22803  prdsxmslem2  22822  metustfbas  22850  icccmplem1  23113  metdstri  23142  pi1addf  23334  pi1addval  23335  caubl  23594  caublcls  23595  relcmpcmet  23604  minveclem4  23718  hlhil  23729  ovolficcss  23753  uniioombllem3a  23868  uniioombllem3  23869  dyadss  23878  opnmbllem  23885  i1fima2  23963  limcfval  24153  dvfval  24178  dvnres  24211  dvivth  24290  lhop  24296  taylf  24632  xrlimcnp  25228  jensen  25248  ppisval  25363  chtlepsi  25464  chpub  25478  iscgrglt  25982  chssoc  28964  mdsl0  29778  mdexchi  29803  atcvat3i  29864  dmdbr5ati  29890  funimass4f  30072  xrofsup  30180  pmtrcnel  30392  tocycfvres1  30399  tocycfvres2  30400  cycpmconjvlem  30420  cycpmconjslem2  30435  fedgmullem1  30629  fedgmullem2  30630  locfinreflem  30721  cmpcref  30731  cnvordtrestixx  30773  ordtrestNEW  30781  ordtrest2NEW  30783  pnfneige0  30811  sigagenss  31025  imambfm  31137  dya2iocress  31149  dya2icoseg  31152  dya2iocucvr  31159  ballotlemro  31397  ftc2re  31486  bnj1097  31867  bnj1452  31938  cvmlift3lem6  32179  msubrn  32384  mclsssv  32419  mclsind  32425  trpredmintr  32679  noextend  32782  nosupbday  32814  scutun12  32880  scutbdaybnd  32884  scutbdaylt  32885  liness  33215  neibastop2lem  33317  opnmbllem0  34459  mblfinlem2  34461  isbndx  34592  isbnd2  34593  ssbnd  34598  heiborlem3  34623  igenmin  34874  lsatlss  35663  lsmsat  35675  lsatfixedN  35676  lssats  35679  lpssat  35680  lssatle  35682  lssat  35683  lsatcvat3  35719  paddssat  36481  paddasslem17  36503  pmodlem2  36514  hlmod1i  36523  pl42lem4N  36649  diassdvaN  37727  dia2dimlem10  37740  cdlemn4a  37866  cdlemn5pre  37867  dihord5apre  37929  lclkrlem2e  38178  lclkrlem2p  38189  lclkrlem2v  38195  lclkrslem2  38205  lclkrs  38206  lcfrlem25  38234  lcfrlem35  38244  mapdval2N  38297  mapdpglem8  38346  mapdpglem13  38351  baerlem3lem2  38377  mapdindp2  38388  hdmap11lem2  38509  elrfi  38776  isnacs3  38792  mzpf  38818  mzpindd  38828  diophrw  38841  eldiophss  38856  rmxyelqirr  38992  pw2f1ocnv  39119  aomclem6  39144  hbt  39215  rgspnmin  39256  cnvssb  39431  trclubgNEW  39463  dfrcl2  39504  fvmptiunrelexplb0da  39515  relexp0a  39546  cotrcltrcl  39555  trclimalb2  39556  cotrclrcl  39572  isotone2  39884  k0004ss1  39986  fnresdmss  40964  mptelpm  40972  ssnnf1octb  40996  uzfissfz  41135  iuneqfzuzlem  41143  xlimliminflimsup  41685  icccncfext  41711  dvnprodlem1  41772  dvnprodlem2  41773  dvnprodlem3  41774  fourierdlem41  41975  fourierdlem70  42003  fourierdlem71  42004  fourierdlem80  42013  fourierdlem113  42046  ioorrnopnlem  42131  ioorrnopnxrlem  42133  salgenss  42161  dfsalgen2  42166  subsaliuncllem  42182  iundjiun  42284  meadjiunlem  42289  meaiunlelem  42292  meaiuninclem  42304  meaiininclem  42310  omeunle  42340  carageniuncllem2  42346  caratheodorylem1  42350  caratheodorylem2  42351  hoissre  42368  ovnsubaddlem1  42394  hoidmvlelem3  42421  ovnhoilem1  42425  ovnhoilem2  42426  ovnhoi  42427  ovncvr2  42435  voncmpl  42445  hspmbllem2  42451  hspmbl  42453  opnvonmbllem1  42456  vonmblss  42464  ovnsubadd2lem  42469  vonioolem2  42505  preimageiingt  42540  preimaleiinlt  42541  issmfd  42554  issmfdf  42556  sssmf  42557  cnfsmf  42559  issmfled  42576  issmfgtd  42579  smfadd  42583  smfrec  42606  smfmul  42612  smfmulc1  42613  smfpimbor1lem2  42616  smfsuplem1  42627  smflimsuplem1  42636  smflimsuplem7  42642  sprssspr  43125  linc1  43960