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

Theorem eqsstri 2969
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.)
Hypotheses
Ref Expression
eqsstr.1 A = B
eqsstr.2 B𝐶
Assertion
Ref Expression
eqsstri A𝐶

Proof of Theorem eqsstri
StepHypRef Expression
1 eqsstr.2 . 2 B𝐶
2 eqsstr.1 . . 3 A = B
32sseq1i 2963 . 2 (A𝐶B𝐶)
41, 3mpbir 134 1 A𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1242  wss 2911
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-11 1394  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-in 2918  df-ss 2925
This theorem is referenced by:  eqsstr3i  2970  ssrab2  3019  rabssab  3021  difdifdirss  3301  opabss  3812  brab2ga  4358  relopabi  4406  dmopabss  4490  resss  4578  relres  4582  exse2  4642  rnin  4676  rnxpss  4697  cnvcnvss  4718  dmmptss  4760  fnres  4958  resasplitss  5012  fabexg  5020  f0  5023  ffvresb  5271  isoini2  5401  dmoprabss  5528  elmpt2cl  5640  tposssxp  5805  dftpos4  5819  smores  5848  smores2  5850  iordsmo  5853  swoer  6070  swoord1  6071  swoord2  6072  ecss  6083  ecopovsym  6138  ecopovtrn  6139  ecopover  6140  ecopovsymg  6141  ecopovtrng  6142  ecopoverg  6143  pinn  6293  niex  6296  ltrelpi  6308  dmaddpi  6309  dmmulpi  6310  enqex  6344  ltrelnq  6349  enq0ex  6422  ltrelpr  6488  enrex  6665  ltrelsr  6666  ltrelre  6730  ltrelxr  6877  lerelxr  6879  nn0ssre  7961  nn0ssz  8039  rpre  8364
  Copyright terms: Public domain W3C validator