Theorem eqsstr 2081

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 2075	. 2 |- (A (_ C <-> B (_ C)
4	1, 3	mpbir 190	1 |- A (_ C

Syntax hints:   = wceq 953   (_ wss 2037

This theorem is referenced by:  eqsstr3 2082  ssrab2 2121  opabss 2658  dmopabss 3310  resss 3367  relres 3371  rnin 3444  cnvcnvss 3474  fabexg 3638  f0 3641  tz6.12-2 3724  fvopab4ndm 3769  dmoprabss 3988  oawordeulem 4172  ecopoprdm 4293  ecopoprsym 4294  ecopoprtrn 4295  sbthlem7 4433  inf3lem1 4585  rankval3 4653  rankuni2 4662  rankuni 4670  rankuniss 4673  cplem1 4692  hta 4700  ac6lem 4726  zorn2lem1 4760  zorn2lem3 4762  zorn2lem4 4763  zorn2lem5 4764  imadomg 4778  pinn 4978  niex 4981  ltrelpi 4989  dmaddpi 4990  dmmulpi 4991  enqex 5020  ltrelpq 5023  dmaddpq 5031  dmmulpq 5033  ltrelpr 5073  enrex 5150  ltrelsr 5152  dmaddsr 5166  dmmulsr 5167  ltrelre 5224  axaddopr 5237  axmulopr 5238  nn0ssre 6050  nn0ssz 6099  rpret 6222  uzssz 6362  sqrlem6 6608  cau5 6856  cvganuz 6862  sumex 6919  caucvglem2 7094  infcvgaux1 7154  ivthlem4 7219  ivthlem5 7220  ivthlem7 7222  ivthlem9 7224  ivthlem4OLD 7228  ivthlem5OLD 7229  ivthlem7OLD 7231  infpn2 7452  subbas 7586  lmbr2 7867  lmbrf 7868  iscau3 7876  iscauf 7877  bcthlem14 7946  issubgi 8059  ghsubgi 8075  nvss 8150  nvvcop 8151  phnv 8404  pilem2 8591  pilem3 8592  circgrpOLD 8658  shftefif1olem 8661  shftefif1olemOLD 8662  explogt 8694  chsssh 9015  projlem8 9109  shscl 9196  shjshs 9330  3oalem4 9527  pjf 9566  dmadjss 9736  nmcopexlem4 9869  nmcfnexlem4 9898  nlelsh 9908  hmopidmch 9990  hmopidmpj 9991  atssch 10178  shatomistic 10196  ghomgrpilem2 10291  dmhmph 10419  rnhmph 10420  1alg 10498  strded 10516  strcat 10537

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-in 2041  df-ss 2043

Copyright terms: Public domain