Theorem sseq1i 3487

Description: An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993.)

Hypothesis

Ref	Expression
sseq1i.1	|- A = B

Assertion

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

Proof of Theorem sseq1i

Step	Hyp	Ref	Expression
1		sseq1i.1	. 2 |- A = B
2		sseq1 3484	. 2 |- ( A = B -> ( A C_ C <-> B C_ C ) )
3	1, 2	ax-mp 5	1 |- ( A C_ C <-> B C_ C )

Syntax hints:   <-> wb 184   = wceq 1370   C_ wss 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3442  df-ss 3449

This theorem is referenced by:  eqsstri  3493  syl5eqss  3507  ssab  3529  rabss  3536  uniiunlem  3547  prss  4134  prssg  4135  sstp  4144  tpss  4145  iunss  4318  pwtr  4652  pwssun  4734  cores2  5457  dffun2  5535  sbcfg  5664  fnsuppresOLD  6046  idref  6066  ovmptss  6763  fnsuppres  6825  ordgt0ge1  7046  omopthlem1  7203  trcl  8058  rankbnd  8185  rankbnd2  8186  rankc1  8187  dfac12a  8427  fin23lem34  8625  axdc2lem  8727  alephval2  8846  indpi  9186  0ram  14198  mreacs  14714  lsslinds  18384  2ndcctbss  19190  xkoinjcn  19391  restmetu  20293  xrlimcnp  22494  mptelee  23292  ausisusgra  23430  shlesb1i  24940  mdsldmd1i  25886  csmdsymi  25889  dfon2lem3  27741  dfon2lem7  27745  sspred  27776  trpredmintr  27838  filnetlem4  28749  frgraunss  30734  n4cyclfrgra  30757  fsuppmapnn0fiublem  30945