Theorem eqsstri 3256

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

Syntax hints:   = wceq 1395   ⊆ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  eqsstrri  3257  ssrab2  3309  ssrab3  3310  rabssab  3312  difdifdirss  3576  ifssun  3617  opabss  4147  brab2ga  4793  relopabi  4846  dmopabss  4934  resss  5028  relres  5032  exse2  5101  rnin  5137  rnxpss  5159  cnvcnvss  5182  dmmptss  5224  cocnvss  5253  fnres  5439  resasplitss  5504  fabexg  5512  f0  5515  ffvresb  5797  isoini2  5942  dmoprabss  6085  elmpocl  6199  tposssxp  6393  dftpos4  6407  smores  6436  smores2  6438  iordsmo  6441  swoer  6706  swoord1  6707  swoord2  6708  ecss  6721  ecopovsym  6776  ecopovtrn  6777  ecopover  6778  ecopovsymg  6779  ecopovtrng  6780  ecopoverg  6781  opabfi  7096  sbthlem7  7126  caserel  7250  ctssdccl  7274  pw1on  7407  pinn  7492  niex  7495  ltrelpi  7507  dmaddpi  7508  dmmulpi  7509  enqex  7543  ltrelnq  7548  enq0ex  7622  ltrelpr  7688  enrex  7920  ltrelsr  7921  ltrelre  8016  axaddf  8051  axmulf  8052  ltrelxr  8203  lerelxr  8205  nn0ssre  9369  nn0ssz  9460  rpre  9852  fz1ssfz0  10309  infssuzcldc  10450  swrd00g  11176  cau3  11621  fsum3cvg3  11902  isumshft  11996  explecnv  12011  clim2prod  12045  ntrivcvgap  12054  dvdszrcl  12298  dvdsflip  12357  phimullem  12742  eulerthlemfi  12745  eulerthlemrprm  12746  eulerthlema  12747  eulerthlemh  12748  eulerthlemth  12749  4sqlem1  12906  4sqlem19  12927  ctiunctlemuom  13002  structcnvcnv  13043  fvsetsid  13061  strleun  13132  dmtopon  14691  lmfval  14860  lmbrf  14883  cnconst2  14901  txuni2  14924  xmeter  15104  ivthinclemex  15310  dvidsslem  15361  dvconstss  15366  dvrecap  15381  lgsquadlemofi  15749  lgsquadlem1  15750  lgsquadlem2  15751  2sqlem7  15794