Theorem sseq1i 2085

Description: An equality inference for the subclass relationship.

Hypothesis

Ref	Expression
sseq1i.1	|- A = B

Assertion

Ref	Expression
sseq1i	|- (A (_ C <-> B (_ C)

Proof of Theorem sseq1i

Step	Hyp	Ref	Expression
1		sseq1i.1	. 2 |- A = B
2		sseq1 2082	. 2 |- (A = B -> (A (_ C <-> B (_ C))
3	1, 2	ax-mp 7	1 |- (A (_ C <-> B (_ C)

Syntax hints:   <-> wb 146   = wceq 956   (_ wss 2047

This theorem is referenced by:  eqsstr 2091  syl5ss 2105  ssab 2118  rabss 2124  uniiunlem 2132  pwssun 2827  cotr 3436  cnvsym 3437  cores2 3507  dffun2 3526  ordgt0ge1 4144  trcl 4645  rankr1 4674  rankbnd 4703  rankbnd2 4704  rankc1 4705  cardne 4830  alephval2 4902  indpi 5034  cnpco 7769  bcthlem32 8030  shlesb1 9359  chsscon2 9386  mdsldmd1 10258  csmdsym 10261

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2051  df-ss 2053

Copyright terms: Public domain