Theorem eqsstri 3188

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

Syntax hints:   = wceq 1353   ⊆ wss 3130

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3136  df-ss 3143

This theorem is referenced by:  eqsstrri  3189  ssrab2  3241  ssrab3  3242  rabssab  3244  difdifdirss  3508  ifssun  3549  opabss  4068  brab2ga  4702  relopabi  4753  dmopabss  4840  resss  4932  relres  4936  exse2  5003  rnin  5039  rnxpss  5061  cnvcnvss  5084  dmmptss  5126  cocnvss  5155  fnres  5333  resasplitss  5396  fabexg  5404  f0  5407  ffvresb  5680  isoini2  5820  dmoprabss  5957  elmpocl  6069  tposssxp  6250  dftpos4  6264  smores  6293  smores2  6295  iordsmo  6298  swoer  6563  swoord1  6564  swoord2  6565  ecss  6576  ecopovsym  6631  ecopovtrn  6632  ecopover  6633  ecopovsymg  6634  ecopovtrng  6635  ecopoverg  6636  sbthlem7  6962  caserel  7086  ctssdccl  7110  pw1on  7225  pinn  7308  niex  7311  ltrelpi  7323  dmaddpi  7324  dmmulpi  7325  enqex  7359  ltrelnq  7364  enq0ex  7438  ltrelpr  7504  enrex  7736  ltrelsr  7737  ltrelre  7832  axaddf  7867  axmulf  7868  ltrelxr  8018  lerelxr  8020  nn0ssre  9180  nn0ssz  9271  rpre  9660  fz1ssfz0  10117  cau3  11124  fsum3cvg3  11404  isumshft  11498  explecnv  11513  clim2prod  11547  ntrivcvgap  11556  dvdszrcl  11799  dvdsflip  11857  infssuzcldc  11952  phimullem  12225  eulerthlemfi  12228  eulerthlemrprm  12229  eulerthlema  12230  eulerthlemh  12231  eulerthlemth  12232  4sqlem1  12386  ctiunctlemuom  12437  structcnvcnv  12478  fvsetsid  12496  strleun  12563  dmtopon  13526  lmfval  13695  lmbrf  13718  cnconst2  13736  txuni2  13759  xmeter  13939  ivthinclemex  14123  dvrecap  14180  2sqlem7  14471