Theorem sseq1d 2088

Description: An equality deduction for the subclass relationship.

Hypothesis

Ref	Expression
sseq1d.1	|- (ph -> A = B)

Assertion

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

Proof of Theorem sseq1d

Step	Hyp	Ref	Expression
1		sseq1d.1	. 2 |- (ph -> A = B)
2		sseq1 2082	. 2 |- (A = B -> (A (_ C <-> B (_ C))
3	1, 2	syl 10	1 |- (ph -> (A (_ C <-> B (_ C))

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

This theorem is referenced by:  sseq12d 2090  eqsstrd 2095  snssg 2463  prssg 2472  ssiun2s 2594  treq 2686  ordunel 3084  dmxpss 3473  rnxpss 3474  funimass1 3572  feq1 3620  fvimacnvi 3804  fvimacnvALT 3809  oaordi 4180  oaword2 4187  oawordeulem 4188  omwordri 4203  omword1 4204  oewordri 4219  oeordsuc 4221  ereq 4267  map0e 4342  sbthlem5 4451  fodomr 4483  inf3lema 4609  inf3lemd 4612  trcl 4645  r1val1 4658  rankr1 4674  rankxplim 4712  scottex 4716  scott0 4717  scottexs 4718  scott0s 4719  karden 4726  cardaleph 4885  cfub 4908  cflecard 4912  cfle 4913  peano5uzt 6204  infmap2lem2 7580  iscnp 7760  cnsscnp 7772  blss 7853  ssblex 7856  opnin 7869  blnei 7879  metcnp 7887  tgioolem 7914  bcthlem9 8007  bcthlem15 8013  bcthlem18 8016  bcthlem28 8026  bcth 8032  subgrnss 8119  sspval 8382  isssp 8383  ocsh 9156  hsupval2t 9300  chsupid 9311  chsupsn 9312  shlubt 9354  shmod 9363  chsscon3t 9423  chsscon2t 9425  spansncv 9597  pj3 10136  mdslmd1lem3 10254  mdslmd1lem4 10255  mdsymlem5 10334  sumdmdlem2 10346  dmdbr5at 10349  dmdbr6at 10350  dmdbr7at 10351  sfvlim 10605  sfvlimOLD 10606  plimfilOLD 10609  iintlem2 10633  isalg 10653  algi 10660

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