Theorem sseq1d 2078

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 2072	. 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 953   (_ wss 2037

This theorem is referenced by:  sseq12d 2080  eqsstrd 2085  snssg 2454  prssg 2463  ssiun2s 2584  treq 2676  ordunel 3074  dmxpss 3459  rnxpss 3460  funimass1 3558  feq1 3606  fvimacnvi 3789  fvimacnvALT 3794  oaordi 4164  oaword2 4171  oawordeulem 4172  omwordri 4187  omword1 4188  oewordri 4203  oeordsuc 4205  ereq 4251  map0e 4326  sbthlem5 4431  fodomr 4463  inf3lema 4581  inf3lemd 4584  trcl 4617  r1val1 4630  rankr1 4646  rankxplim 4684  scottex 4688  scott0 4689  scottexs 4690  scott0s 4691  karden 4698  cardaleph 4857  cfub 4880  cflecard 4884  cfle 4885  peano5uzt 6152  infmap2lem2 7522  iscnp 7700  cnsscnp 7711  blss 7793  ssblex 7796  opnin 7809  blnei 7818  metcnp 7826  tgioolem 7853  bcthlem9 7941  bcthlem15 7947  bcthlem18 7950  bcthlem28 7960  bcth 7966  subgrnss 8056  sspval 8316  isssp 8317  ocsh 9072  hsupval2t 9215  chsupid 9226  chsupsn 9227  shlubt 9269  shmod 9278  chsscon3t 9338  chsscon2t 9340  spansncv 9514  pj3 10046  mdslmd1lem3 10162  mdslmd1lem4 10163  mdsymlem5 10242  sumdmdlem2 10253  dmdbr5at 10255  dmdbr6at 10256  iintlem2 10477  isalg 10497  algi 10504

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