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 1533   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  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  6968  tfisi  7567  suppssof1  7857  suppss2  7858  onfununi  7972  oawordeulem  8174  oeeui  8222  nnawordex  8257  oaabslem  8264  oaabs2  8266  omabslem  8267  omabs  8268  pw2f1olem  8615  fodomr  8662  fival  8870  dffi3  8889  ordtypelem7  8982  ordtypelem8  8983  wemapso2lem  9010  cantnflt2  9130  cantnflem1  9146  tcss  9180  tcel  9181  r1val1  9209  rankuni2b  9276  tcrank  9307  cardonle  9380  harval2  9420  ackbij2  9659  cfub  9665  cflecard  9669  cfflb  9675  isf32lem8  9776  itunitc1  9836  ttukeylem7  9931  fpwwe2lem9  10054  wuncss  10161  wuncval2  10163  grur1a  10235  trclfvub  14361  cotrtrclfv  14366  relexpfld  14402  rtrclreclem4  14414  limsupgre  14832  isercolllem3  15017  4sqlem19  16293  vdwlem1  16311  vdwlem12  16322  ramub1lem1  16356  setsstruct2  16515  ressress  16556  imasaddfnlem  16795  imasaddflem  16797  imasvscafn  16804  imasvscaf  16806  imasless  16807  isohom  17040  ressffth  17202  acsfiindd  17781  acsmap2d  17783  dirref  17839  mndind  17986  f1omvdco2  18570  pmtrfrn  18580  symgsssg  18589  symggen  18592  psgnunilem1  18615  sylow2alem2  18737  lsmssv  18762  smndlsmidm  18775  lsmidmOLD  18783  gsumzres  19023  dprdlub  19142  dprdf1  19149  dprdsn  19152  dprdcntz2  19154  dprd2dlem1  19157  dprd2da  19158  dmdprdsplit2lem  19161  ablfac1eu  19189  drnglpir  20020  issubassa2  20115  evlslem4  20282  evlseu  20290  mhpaddcl  20332  mhpinvcl  20333  znleval  20695  evpmss  20724  frlmsplit2  20911  f1lindf  20960  lpsscls  21743  tgrest  21761  resttopon  21763  rest0  21771  restfpw  21781  ordtrest  21804  ordtrest2  21806  lmcnp  21906  tgcmp  22003  uncmp  22005  hauscmplem  22008  1stcfb  22047  2ndcdisj  22058  dissnref  22130  kgencmp  22147  xkouni  22201  prdstopn  22230  txtube  22242  txcmplem2  22244  xkoptsub  22256  xkopt  22257  xkococnlem  22261  qtoprest  22319  imastopn  22322  kqdisj  22334  reghmph  22395  nrmhmph  22396  fbssfi  22439  trfilss  22491  trfg  22493  elfm3  22552  alexsubALTlem3  22651  alexsubALT  22653  cnextf  22668  cnextcn  22669  clsnsg  22712  tgpconncompeqg  22714  qustgphaus  22725  trust  22832  ustuqtop3  22846  neipcfilu  22899  metequiv2  23114  prdsxmslem2  23133  metustfbas  23161  icccmplem1  23424  metdstri  23453  pi1addf  23645  pi1addval  23646  caubl  23905  caublcls  23906  relcmpcmet  23915  minveclem4  24029  hlhil  24040  ovolficcss  24064  uniioombllem3a  24179  uniioombllem3  24180  dyadss  24189  opnmbllem  24196  i1fima2  24274  limcfval  24464  dvfval  24489  dvnres  24522  dvivth  24601  lhop  24607  taylf  24943  xrlimcnp  25540  jensen  25560  ppisval  25675  chtlepsi  25776  chpub  25790  iscgrglt  26294  chssoc  29267  mdsl0  30081  mdexchi  30106  atcvat3i  30167  dmdbr5ati  30193  funimass4f  30376  xrofsup  30486  swrdrn2  30623  pmtrcnel  30728  tocycfvres1  30747  tocycfvres2  30748  cycpmco2lem6  30768  cycpmconjvlem  30778  cycpmconjslem2  30792  fedgmullem1  31020  fedgmullem2  31021  locfinreflem  31099  cmpcref  31109  cnvordtrestixx  31151  ordtrestNEW  31159  ordtrest2NEW  31161  pnfneige0  31189  sigagenss  31403  imambfm  31515  dya2iocress  31527  dya2icoseg  31530  dya2iocucvr  31537  ballotlemro  31775  ftc2re  31864  bnj1097  32248  bnj1452  32319  cvmlift3lem6  32566  msubrn  32771  mclsssv  32806  mclsind  32812  trpredmintr  33065  noextend  33168  nosupbday  33200  scutun12  33266  scutbdaybnd  33270  scutbdaylt  33271  liness  33601  neibastop2lem  33703  opnmbllem0  34922  mblfinlem2  34924  isbndx  35054  isbnd2  35055  ssbnd  35060  heiborlem3  35085  igenmin  35336  lsatlss  36126  lsmsat  36138  lsatfixedN  36139  lssats  36142  lpssat  36143  lssatle  36145  lssat  36146  lsatcvat3  36182  paddssat  36944  paddasslem17  36966  pmodlem2  36977  hlmod1i  36986  pl42lem4N  37112  diassdvaN  38190  dia2dimlem10  38203  cdlemn4a  38329  cdlemn5pre  38330  dihord5apre  38392  lclkrlem2e  38641  lclkrlem2p  38652  lclkrlem2v  38658  lclkrslem2  38668  lclkrs  38669  lcfrlem25  38697  lcfrlem35  38707  mapdval2N  38760  mapdpglem8  38809  mapdpglem13  38814  baerlem3lem2  38840  mapdindp2  38851  hdmap11lem2  38972  elrfi  39284  isnacs3  39300  mzpf  39326  mzpindd  39336  diophrw  39349  eldiophss  39364  rmxyelqirr  39500  pw2f1ocnv  39627  aomclem6  39652  hbt  39723  rgspnmin  39764  cnvssb  39939  trclubgNEW  39971  dfrcl2  40012  fvmptiunrelexplb0da  40023  relexp0a  40054  cotrcltrcl  40063  trclimalb2  40064  cotrclrcl  40080  isotone2  40392  k0004ss1  40494  fnresdmss  41416  mptelpm  41424  ssnnf1octb  41448  uzfissfz  41586  iuneqfzuzlem  41594  xlimliminflimsup  42135  icccncfext  42162  dvnprodlem1  42223  dvnprodlem2  42224  dvnprodlem3  42225  fourierdlem41  42426  fourierdlem70  42454  fourierdlem71  42455  fourierdlem80  42464  fourierdlem113  42497  ioorrnopnlem  42582  ioorrnopnxrlem  42584  salgenss  42612  dfsalgen2  42617  subsaliuncllem  42633  iundjiun  42735  meadjiunlem  42740  meaiunlelem  42743  meaiuninclem  42755  meaiininclem  42761  omeunle  42791  carageniuncllem2  42797  caratheodorylem1  42801  caratheodorylem2  42802  hoissre  42819  ovnsubaddlem1  42845  hoidmvlelem3  42872  ovnhoilem1  42876  ovnhoilem2  42877  ovnhoi  42878  ovncvr2  42886  voncmpl  42896  hspmbllem2  42902  hspmbl  42904  opnvonmbllem1  42907  vonmblss  42915  ovnsubadd2lem  42920  vonioolem2  42956  preimageiingt  42991  preimaleiinlt  42992  issmfd  43005  issmfdf  43007  sssmf  43008  cnfsmf  43010  issmfled  43027  issmfgtd  43030  smfadd  43034  smfrec  43057  smfmul  43063  smfmulc1  43064  smfpimbor1lem2  43067  smfsuplem1  43078  smflimsuplem1  43087  smflimsuplem7  43093  sprssspr  43636  linc1  44473