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

Theorem sseq1d 3126
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 3120 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2syl 14 1 (𝜑 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1331  wss 3071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084
This theorem is referenced by:  sseq12d  3128  eqsstrd  3133  snssg  3656  ssiun2s  3857  treq  4032  onsucsssucexmid  4442  funimass1  5200  feq1  5255  sbcfg  5271  fvmptssdm  5505  fvimacnvi  5534  nnsucsssuc  6388  ereq1  6436  elpm2r  6560  fipwssg  6867  nnnninf  7023  ctssexmid  7024  iscnp  12382  iscnp4  12401  cnntr  12408  cnconst2  12416  cnptopresti  12421  cnptoprest  12422  txbas  12441  txcnp  12454  txdis  12460  txdis1cn  12461  blssps  12610  blss  12611  ssblex  12614  blin2  12615  metss2  12681  metrest  12689  metcnp3  12694  cnopnap  12777  limccl  12811  ellimc3apf  12812
  Copyright terms: Public domain W3C validator