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

Theorem sseqtrrd 3232
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
sseqtrrd.1  |-  ( ph  ->  A  C_  B )
sseqtrrd.2  |-  ( ph  ->  C  =  B )
Assertion
Ref Expression
sseqtrrd  |-  ( ph  ->  A  C_  C )

Proof of Theorem sseqtrrd
StepHypRef Expression
1 sseqtrrd.1 . 2  |-  ( ph  ->  A  C_  B )
2 sseqtrrd.2 . . 3  |-  ( ph  ->  C  =  B )
32eqcomd 2211 . 2  |-  ( ph  ->  B  =  C )
41, 3sseqtrd 3231 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1373    C_ wss 3166
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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187
This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179
This theorem is referenced by:  sseqtrrid  3244  fnfvima  5819  tfrlemiubacc  6416  tfr1onlemubacc  6432  tfrcllemubacc  6445  rdgivallem  6467  nnnninf  7228  nninfwlpoimlemg  7277  ccatass  11064  swrdval2  11104  dfphi2  12542  ctinf  12801  imasaddfnlemg  13146  imasaddvallemg  13147  subsubm  13315  subsubg  13533  subsubrng  13976  subsubrg  14007  lidlss  14238  toponss  14498  ssntr  14594  iscnp3  14675  cnprcl2k  14678  tgcn  14680  tgcnp  14681  ssidcn  14682  cncnp  14702  txcnp  14743  imasnopn  14771  hmeontr  14785  blssec  14910  blssopn  14957  xmettx  14982  metcnp  14984  plyaddlem1  15219  plymullem1  15220  plycoeid3  15229  nnsf  15942  nninfsellemsuc  15949
  Copyright terms: Public domain W3C validator