Theorem eqsstrd 4005

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  eqsstrrd  4006  eqsstrdi  4021  fpr2g  6974  tfisi  7573  suppssof1  7863  suppss2  7864  onfununi  7978  oawordeulem  8180  oeeui  8228  nnawordex  8263  oaabslem  8270  oaabs2  8272  omabslem  8273  omabs  8274  pw2f1olem  8621  fodomr  8668  fival  8876  dffi3  8895  ordtypelem7  8988  ordtypelem8  8989  wemapso2lem  9016  cantnflt2  9136  cantnflem1  9152  tcss  9186  tcel  9187  r1val1  9215  rankuni2b  9282  tcrank  9313  cardonle  9386  harval2  9426  ackbij2  9665  cfub  9671  cflecard  9675  cfflb  9681  isf32lem8  9782  itunitc1  9842  ttukeylem7  9937  fpwwe2lem9  10060  wuncss  10167  wuncval2  10169  grur1a  10241  trclfvub  14367  cotrtrclfv  14372  relexpfld  14408  rtrclreclem4  14420  limsupgre  14838  isercolllem3  15023  4sqlem19  16299  vdwlem1  16317  vdwlem12  16328  ramub1lem1  16362  setsstruct2  16521  ressress  16562  imasaddfnlem  16801  imasaddflem  16803  imasvscafn  16810  imasvscaf  16812  imasless  16813  isohom  17046  ressffth  17208  acsfiindd  17787  acsmap2d  17789  dirref  17845  mndind  17992  f1omvdco2  18576  pmtrfrn  18586  symgsssg  18595  symggen  18598  psgnunilem1  18621  sylow2alem2  18743  lsmssv  18768  smndlsmidm  18781  lsmidmOLD  18789  gsumzres  19029  dprdlub  19148  dprdf1  19155  dprdsn  19158  dprdcntz2  19160  dprd2dlem1  19163  dprd2da  19164  dmdprdsplit2lem  19167  ablfac1eu  19195  drnglpir  20026  issubassa2  20121  evlslem4  20288  evlseu  20296  mhpaddcl  20338  mhpinvcl  20339  znleval  20701  evpmss  20730  frlmsplit2  20917  f1lindf  20966  lpsscls  21749  tgrest  21767  resttopon  21769  rest0  21777  restfpw  21787  ordtrest  21810  ordtrest2  21812  lmcnp  21912  tgcmp  22009  uncmp  22011  hauscmplem  22014  1stcfb  22053  2ndcdisj  22064  dissnref  22136  kgencmp  22153  xkouni  22207  prdstopn  22236  txtube  22248  txcmplem2  22250  xkoptsub  22262  xkopt  22263  xkococnlem  22267  qtoprest  22325  imastopn  22328  kqdisj  22340  reghmph  22401  nrmhmph  22402  fbssfi  22445  trfilss  22497  trfg  22499  elfm3  22558  alexsubALTlem3  22657  alexsubALT  22659  cnextf  22674  cnextcn  22675  clsnsg  22718  tgpconncompeqg  22720  qustgphaus  22731  trust  22838  ustuqtop3  22852  neipcfilu  22905  metequiv2  23120  prdsxmslem2  23139  metustfbas  23167  icccmplem1  23430  metdstri  23459  pi1addf  23651  pi1addval  23652  caubl  23911  caublcls  23912  relcmpcmet  23921  minveclem4  24035  hlhil  24046  ovolficcss  24070  uniioombllem3a  24185  uniioombllem3  24186  dyadss  24195  opnmbllem  24202  i1fima2  24280  limcfval  24470  dvfval  24495  dvnres  24528  dvivth  24607  lhop  24613  taylf  24949  xrlimcnp  25546  jensen  25566  ppisval  25681  chtlepsi  25782  chpub  25796  iscgrglt  26300  chssoc  29273  mdsl0  30087  mdexchi  30112  atcvat3i  30173  dmdbr5ati  30199  funimass4f  30382  xrofsup  30492  swrdrn2  30628  pmtrcnel  30733  tocycfvres1  30752  tocycfvres2  30753  cycpmco2lem6  30773  cycpmconjvlem  30783  cycpmconjslem2  30797  fedgmullem1  31025  fedgmullem2  31026  locfinreflem  31104  cmpcref  31114  cnvordtrestixx  31156  ordtrestNEW  31164  ordtrest2NEW  31166  pnfneige0  31194  sigagenss  31408  imambfm  31520  dya2iocress  31532  dya2icoseg  31535  dya2iocucvr  31542  ballotlemro  31780  ftc2re  31869  bnj1097  32253  bnj1452  32324  cvmlift3lem6  32571  msubrn  32776  mclsssv  32811  mclsind  32817  trpredmintr  33070  noextend  33173  nosupbday  33205  scutun12  33271  scutbdaybnd  33275  scutbdaylt  33276  liness  33606  neibastop2lem  33708  opnmbllem0  34943  mblfinlem2  34945  isbndx  35075  isbnd2  35076  ssbnd  35081  heiborlem3  35106  igenmin  35357  lsatlss  36147  lsmsat  36159  lsatfixedN  36160  lssats  36163  lpssat  36164  lssatle  36166  lssat  36167  lsatcvat3  36203  paddssat  36965  paddasslem17  36987  pmodlem2  36998  hlmod1i  37007  pl42lem4N  37133  diassdvaN  38211  dia2dimlem10  38224  cdlemn4a  38350  cdlemn5pre  38351  dihord5apre  38413  lclkrlem2e  38662  lclkrlem2p  38673  lclkrlem2v  38679  lclkrslem2  38689  lclkrs  38690  lcfrlem25  38718  lcfrlem35  38728  mapdval2N  38781  mapdpglem8  38830  mapdpglem13  38835  baerlem3lem2  38861  mapdindp2  38872  hdmap11lem2  38993  elrfi  39340  isnacs3  39356  mzpf  39382  mzpindd  39392  diophrw  39405  eldiophss  39420  rmxyelqirr  39556  pw2f1ocnv  39683  aomclem6  39708  hbt  39779  rgspnmin  39820  cnvssb  39995  trclubgNEW  40027  dfrcl2  40068  fvmptiunrelexplb0da  40079  relexp0a  40110  cotrcltrcl  40119  trclimalb2  40120  cotrclrcl  40136  isotone2  40448  k0004ss1  40550  fnresdmss  41473  mptelpm  41481  ssnnf1octb  41505  uzfissfz  41643  iuneqfzuzlem  41651  xlimliminflimsup  42192  icccncfext  42219  dvnprodlem1  42280  dvnprodlem2  42281  dvnprodlem3  42282  fourierdlem41  42482  fourierdlem70  42510  fourierdlem71  42511  fourierdlem80  42520  fourierdlem113  42553  ioorrnopnlem  42638  ioorrnopnxrlem  42640  salgenss  42668  dfsalgen2  42673  subsaliuncllem  42689  iundjiun  42791  meadjiunlem  42796  meaiunlelem  42799  meaiuninclem  42811  meaiininclem  42817  omeunle  42847  carageniuncllem2  42853  caratheodorylem1  42857  caratheodorylem2  42858  hoissre  42875  ovnsubaddlem1  42901  hoidmvlelem3  42928  ovnhoilem1  42932  ovnhoilem2  42933  ovnhoi  42934  ovncvr2  42942  voncmpl  42952  hspmbllem2  42958  hspmbl  42960  opnvonmbllem1  42963  vonmblss  42971  ovnsubadd2lem  42976  vonioolem2  43012  preimageiingt  43047  preimaleiinlt  43048  issmfd  43061  issmfdf  43063  sssmf  43064  cnfsmf  43066  issmfled  43083  issmfgtd  43086  smfadd  43090  smfrec  43113  smfmul  43119  smfmulc1  43120  smfpimbor1lem2  43123  smfsuplem1  43134  smflimsuplem1  43143  smflimsuplem7  43149  sprssspr  43692  linc1  44529