Theorem eqsstri 3229

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.)

Hypotheses

Ref	Expression
eqsstr.1	⊢ 𝐴 = 𝐵
eqsstr.2	⊢ 𝐵 ⊆ 𝐶

Assertion

Ref	Expression
eqsstri	⊢ 𝐴 ⊆ 𝐶

Proof of Theorem eqsstri

Step	Hyp	Ref	Expression
1		eqsstr.2	. 2 ⊢ 𝐵 ⊆ 𝐶
2		eqsstr.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	sseq1i 3223	. 2 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)
4	1, 3	mpbir 146	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1373   ⊆ wss 3170

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3176  df-ss 3183

This theorem is referenced by:  eqsstrri  3230  ssrab2  3282  ssrab3  3283  rabssab  3285  difdifdirss  3549  ifssun  3590  opabss  4116  brab2ga  4758  relopabi  4811  dmopabss  4899  resss  4992  relres  4996  exse2  5065  rnin  5101  rnxpss  5123  cnvcnvss  5146  dmmptss  5188  cocnvss  5217  fnres  5402  resasplitss  5467  fabexg  5475  f0  5478  ffvresb  5756  isoini2  5901  dmoprabss  6040  elmpocl  6154  tposssxp  6348  dftpos4  6362  smores  6391  smores2  6393  iordsmo  6396  swoer  6661  swoord1  6662  swoord2  6663  ecss  6676  ecopovsym  6731  ecopovtrn  6732  ecopover  6733  ecopovsymg  6734  ecopovtrng  6735  ecopoverg  6736  opabfi  7050  sbthlem7  7080  caserel  7204  ctssdccl  7228  pw1on  7357  pinn  7442  niex  7445  ltrelpi  7457  dmaddpi  7458  dmmulpi  7459  enqex  7493  ltrelnq  7498  enq0ex  7572  ltrelpr  7638  enrex  7870  ltrelsr  7871  ltrelre  7966  axaddf  8001  axmulf  8002  ltrelxr  8153  lerelxr  8155  nn0ssre  9319  nn0ssz  9410  rpre  9802  fz1ssfz0  10259  infssuzcldc  10400  swrd00g  11125  cau3  11501  fsum3cvg3  11782  isumshft  11876  explecnv  11891  clim2prod  11925  ntrivcvgap  11934  dvdszrcl  12178  dvdsflip  12237  phimullem  12622  eulerthlemfi  12625  eulerthlemrprm  12626  eulerthlema  12627  eulerthlemh  12628  eulerthlemth  12629  4sqlem1  12786  4sqlem19  12807  ctiunctlemuom  12882  structcnvcnv  12923  fvsetsid  12941  strleun  13011  dmtopon  14570  lmfval  14739  lmbrf  14762  cnconst2  14780  txuni2  14803  xmeter  14983  ivthinclemex  15189  dvidsslem  15240  dvconstss  15245  dvrecap  15260  lgsquadlemofi  15628  lgsquadlem1  15629  lgsquadlem2  15630  2sqlem7  15673