Theorem eqsstr 2088

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

Syntax hints:   = wceq 955   (_ wss 2044

This theorem is referenced by:  eqsstr3 2089  ssrab2 2128  opabss 2664  dmopabss 3317  resss 3379  relres 3383  rnin 3454  cnvcnvss 3484  fabexg 3648  f0 3651  tz6.12-2 3734  fvopab4ndm 3779  dmoprabss 3998  oawordeulem 4181  ecopoprdm 4302  ecopoprsym 4303  ecopoprtrn 4304  sbthlem7 4442  inf3lem1 4596  rankval3 4664  rankuni2 4673  rankuni 4681  rankuniss 4684  cplem1 4703  hta 4711  ac6lem 4737  zorn2lem1 4771  zorn2lem3 4773  zorn2lem4 4774  zorn2lem5 4775  imadomg 4789  pinn 4989  niex 4992  ltrelpi 5000  dmaddpi 5001  dmmulpi 5002  enqex 5031  ltrelpq 5034  dmaddpq 5042  dmmulpq 5044  ltrelpr 5084  enrex 5161  ltrelsr 5163  dmaddsr 5177  dmmulsr 5178  ltrelre 5235  axaddopr 5248  axmulopr 5249  nn0ssre 6060  nn0ssz 6109  rpret 6234  uzssz 6375  sqrlem6 6623  cau5 6871  cvganuz 6877  sumex 6934  caucvglem2 7111  infcvgaux1 7171  ivthlem4 7236  ivthlem5 7237  ivthlem7 7239  ivthlem9 7241  ivthlem4OLD 7245  ivthlem5OLD 7246  ivthlem7OLD 7248  infpn2 7469  subbas 7604  lmbr2 7891  lmbrf 7892  iscau3 7900  iscauf 7901  bcthlem14 7974  issubgi 8086  ghsubgi 8102  nvss 8176  nvvcop 8177  phnv 8432  pilem2 8626  pilem3 8627  circgrpOLD 8693  shftefif1olem 8696  explogt 8727  chsssh 9049  projlem8 9148  shscl 9236  shjshs 9370  3oalem4 9567  pjf 9606  dmadjss 9776  nmcopexlem4 9910  nmcfnexlem4 9939  nlelsh 9949  hmopidmch 10035  hmopidmpj 10036  atssch 10226  shatomistic 10244  ghomgrpilem2 10342  dmhmph 10478  rnhmph 10479  1alg 10570  strded 10588  strcat 10609

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-in 2048  df-ss 2050

Copyright terms: Public domain