Theorem eqsstri 3129

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 3123	. 2 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)
4	1, 3	mpbir 145	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1331   ⊆ wss 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084

This theorem is referenced by:  eqsstrri  3130  ssrab2  3182  rabssab  3184  difdifdirss  3447  opabss  3992  brab2ga  4614  relopabi  4665  dmopabss  4751  resss  4843  relres  4847  exse2  4913  rnin  4948  rnxpss  4970  cnvcnvss  4993  dmmptss  5035  cocnvss  5064  fnres  5239  resasplitss  5302  fabexg  5310  f0  5313  ffvresb  5583  isoini2  5720  dmoprabss  5853  elmpocl  5968  tposssxp  6146  dftpos4  6160  smores  6189  smores2  6191  iordsmo  6194  swoer  6457  swoord1  6458  swoord2  6459  ecss  6470  ecopovsym  6525  ecopovtrn  6526  ecopover  6527  ecopovsymg  6528  ecopovtrng  6529  ecopoverg  6530  sbthlem7  6851  caserel  6972  ctssdccl  6996  pinn  7117  niex  7120  ltrelpi  7132  dmaddpi  7133  dmmulpi  7134  enqex  7168  ltrelnq  7173  enq0ex  7247  ltrelpr  7313  enrex  7545  ltrelsr  7546  ltrelre  7641  axaddf  7676  axmulf  7677  ltrelxr  7825  lerelxr  7827  nn0ssre  8981  nn0ssz  9072  rpre  9448  fz1ssfz0  9897  cau3  10887  fsum3cvg3  11165  isumshft  11259  explecnv  11274  clim2prod  11308  ntrivcvgap  11317  dvdszrcl  11498  dvdsflip  11549  infssuzcldc  11644  phimullem  11901  ctiunctlemuom  11949  structcnvcnv  11975  fvsetsid  11993  strleun  12048  dmtopon  12190  lmfval  12361  lmbrf  12384  cnconst2  12402  txuni2  12425  xmeter  12605  ivthinclemex  12789  dvrecap  12846