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

Theorem eqsstrd 3137
 Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
eqsstrd.1 (𝜑𝐴 = 𝐵)
eqsstrd.2 (𝜑𝐵𝐶)
Assertion
Ref Expression
eqsstrd (𝜑𝐴𝐶)

Proof of Theorem eqsstrd
StepHypRef Expression
1 eqsstrd.2 . 2 (𝜑𝐵𝐶)
2 eqsstrd.1 . . 3 (𝜑𝐴 = 𝐵)
32sseq1d 3130 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mpbird 166 1 (𝜑𝐴𝐶)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1332   ⊆ wss 3075 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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3081  df-ss 3088 This theorem is referenced by:  eqsstrrd  3138  eqsstrdi  3153  tfisi  4508  funresdfunsnss  5630  suppssof1  6006  phplem4dom  6763  fival  6865  fiuni  6873  cardonle  7059  exmidfodomrlemim  7073  frecuzrdgtclt  10224  ennnfonelemkh  11959  ennnfonelemf1  11965  strfvssn  12018  setscom  12036  tgrest  12375  resttopon  12377  rest0  12385  lmtopcnp  12456  metequiv2  12702  xmettx  12716  ellimc3apf  12835  dvfvalap  12856  dvcjbr  12878  dvcj  12879  dvfre  12880  nnsf  13372
 Copyright terms: Public domain W3C validator