ILE Home 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