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

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

Proof of Theorem eqsstrrd
StepHypRef Expression
1 eqsstrrd.1 . . 3  |-  ( ph  ->  B  =  A )
21eqcomd 2121 . 2  |-  ( ph  ->  A  =  B )
3 eqsstrrd.2 . 2  |-  ( ph  ->  B  C_  C )
42, 3eqsstrd 3101 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1314    C_ 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:  ssxpbm  4942  ssxp1  4943  ssxp2  4944  suppssof1  5965  tfrlemiubacc  6193  tfr1onlemubacc  6209  tfrcllemubacc  6222  oaword1  6333  phplem4dom  6722  fisseneq  6786  archnqq  7189  epttop  12154  metequiv2  12560  limccnpcntop  12687  limccnp2lem  12688  limccnp2cntop  12689  nnsf  13001
  Copyright terms: Public domain W3C validator