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

Theorem sseq2d 3095
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 3089 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2syl 14 1 (𝜑 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1314  wss 3039
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 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-in 3045  df-ss 3052
This theorem is referenced by:  sseq12d  3096  sseqtrd  3103  exmidsssn  4093  exmidsssnc  4094  onsucsssucexmid  4410  sbcrel  4593  funimass2  5169  fnco  5199  fnssresb  5203  fnimaeq0  5212  foimacnv  5351  fvelimab  5443  ssimaexg  5449  fvmptss2  5462  rdgss  6246  summodclem2  11091  summodc  11092  zsumdc  11093  fsum3cvg3  11105  ennnfoneleminc  11819  isbasisg  12106  tgval  12113  tgss3  12142  restbasg  12232  tgrest  12233  restopn2  12247  cnpnei  12283  cnptopresti  12302  txbas  12322  elmopn  12510  neibl  12555  dvfgg  12709
  Copyright terms: Public domain W3C validator