Theorem eqsstri 3211

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

Hypotheses

Ref	Expression
eqsstr.1	|- A = B
eqsstr.2	|- B C_ C

Assertion

Ref	Expression
eqsstri	|- A C_ C

Proof of Theorem eqsstri

Step	Hyp	Ref	Expression
1		eqsstr.2	. 2 |- B C_ C
2		eqsstr.1	. . 3 |- A = B
3	2	sseq1i 3205	. 2 |- ( A C_ C <-> B C_ C )
4	1, 3	mpbir 146	1 |- A C_ C

Syntax hints:   = wceq 1364   C_ wss 3153

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3159  df-ss 3166

This theorem is referenced by:  eqsstrri  3212  ssrab2  3264  ssrab3  3265  rabssab  3267  difdifdirss  3531  ifssun  3571  opabss  4093  brab2ga  4734  relopabi  4787  dmopabss  4874  resss  4966  relres  4970  exse2  5039  rnin  5075  rnxpss  5097  cnvcnvss  5120  dmmptss  5162  cocnvss  5191  fnres  5370  resasplitss  5433  fabexg  5441  f0  5444  ffvresb  5721  isoini2  5862  dmoprabss  6000  elmpocl  6113  tposssxp  6302  dftpos4  6316  smores  6345  smores2  6347  iordsmo  6350  swoer  6615  swoord1  6616  swoord2  6617  ecss  6630  ecopovsym  6685  ecopovtrn  6686  ecopover  6687  ecopovsymg  6688  ecopovtrng  6689  ecopoverg  6690  opabfi  6992  sbthlem7  7022  caserel  7146  ctssdccl  7170  pw1on  7286  pinn  7369  niex  7372  ltrelpi  7384  dmaddpi  7385  dmmulpi  7386  enqex  7420  ltrelnq  7425  enq0ex  7499  ltrelpr  7565  enrex  7797  ltrelsr  7798  ltrelre  7893  axaddf  7928  axmulf  7929  ltrelxr  8080  lerelxr  8082  nn0ssre  9244  nn0ssz  9335  rpre  9726  fz1ssfz0  10183  cau3  11259  fsum3cvg3  11539  isumshft  11633  explecnv  11648  clim2prod  11682  ntrivcvgap  11691  dvdszrcl  11935  dvdsflip  11993  infssuzcldc  12088  phimullem  12363  eulerthlemfi  12366  eulerthlemrprm  12367  eulerthlema  12368  eulerthlemh  12369  eulerthlemth  12370  4sqlem1  12526  4sqlem19  12547  ctiunctlemuom  12593  structcnvcnv  12634  fvsetsid  12652  strleun  12722  dmtopon  14191  lmfval  14360  lmbrf  14383  cnconst2  14401  txuni2  14424  xmeter  14604  ivthinclemex  14796  dvrecap  14862  lgsquadlem1  15191  2sqlem7  15208