Theorem eqsstr 1530

Description: Substitution of equality into a subclass relationship.

Hypotheses

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

Assertion

Ref	Expression
eqsstr	|- A (_ C

Proof of Theorem eqsstr

Step	Hyp	Ref	Expression
1		eqsstr.2	. 2 |- B (_ C
2		eqsstr.1	. . 3 |- A = B
3	2	sseq1i 1524	. 2 |- (A (_ C <-> B (_ C)
4	1, 3	mpbir 165	1 |- A (_ C

Syntax hints:   = wceq 1091   (_ wss 1487

This theorem is referenced by:  eqsstr3 1531  ssrab 1556  opabss 2100  dmopabss 2540  dmexg 2551  rnexg 2569  resss 2587  relres 2591  rnin 2645  cnvcnvss 2662  funi 2692  f0 2772  tz6.12-2 2845  tz7.48-2 2995  dmoprabss 3032  oawordeulem 3156  ecopoprdm 3245  ecopoprsym 3246  ecopoprtrn 3247  sbthlem7 3355  inf3lem1 3464  rankval3 3525  rankuni 3533  rankuniss 3534  cplem1 3545  ac6lem 3575  zornlem1 3603  zornlem3 3605  zornlem4 3606  zornlem5 3607  imadomg 3616  hta 3619  pinn 3800  niex 3803  ltrelpi 3811  dmaddpi 3812  dmmulpi 3813  enqex 3842  ltrelpq 3845  dmaddpq 3853  dmmulpq 3855  ltrelpr 3895  enrex 3972  ltrelsr 3974  dmaddsr 3988  dmmulsr 3989  ltrelre 4046  nn0ssre 4538  nn0ssz 4578  sqrlem6 4736  fac0 4871  chsssh 5129  projlem8 5200  shscl 5282  shjshs 5412  5oa 5551  3oalem4 5555  pjf 5588  atssch 5741

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-in 1491  df-ss 1492

metamath.org