ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sseq1d GIF version

Theorem sseq1d 3076
Description: An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
Hypothesis
Ref Expression
sseq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
sseq1d (𝜑 → (𝐴𝐶𝐵𝐶))

Proof of Theorem sseq1d
StepHypRef Expression
1 sseq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 sseq1 3070 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2syl 14 1 (𝜑 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1299  wss 3021
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-11 1452  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082
This theorem depends on definitions:  df-bi 116  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-in 3027  df-ss 3034
This theorem is referenced by:  sseq12d  3078  eqsstrd  3083  snssg  3603  ssiun2s  3804  treq  3972  onsucsssucexmid  4380  funimass1  5136  feq1  5191  sbcfg  5207  fvmptssdm  5437  fvimacnvi  5466  nnsucsssuc  6318  ereq1  6366  elpm2r  6490  nnnninf  6935  ctssexmid  6936  iscnp  12149  iscnp4  12168  cnntr  12175  cnconst2  12183  cnptopresti  12188  cnptoprest  12189  txbas  12208  txcnp  12221  txdis  12227  txdis1cn  12228  blssps  12355  blss  12356  ssblex  12359  blin2  12360  metss2  12426  metrest  12434  metcnp3  12435  limccl  12510  ellimc3ap  12511
  Copyright terms: Public domain W3C validator