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

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

Proof of Theorem sseq2d
StepHypRef Expression
1 sseq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 sseq2 3177 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2syl 14 1 (𝜑 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105   = wceq 1353  wss 3127
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-11 1504  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157
This theorem depends on definitions:  df-bi 117  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-in 3133  df-ss 3140
This theorem is referenced by:  sseq12d  3184  sseqtrd  3191  exmidsssn  4197  exmidsssnc  4198  onsucsssucexmid  4520  sbcrel  4706  funimass2  5286  fnco  5316  fnssresb  5320  fnimaeq0  5329  foimacnv  5471  fvelimab  5564  ssimaexg  5570  fvmptss2  5583  rdgss  6374  summodclem2  11357  summodc  11358  zsumdc  11359  fsum3cvg3  11371  prodmodclem2  11552  prodmodc  11553  zproddc  11554  ennnfoneleminc  12378  isbasisg  13035  tgval  13042  tgss3  13071  restbasg  13161  tgrest  13162  restopn2  13176  cnpnei  13212  cnptopresti  13231  txbas  13251  elmopn  13439  neibl  13484  dvfgg  13650
  Copyright terms: Public domain W3C validator