MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3sstr4g Unicode version

Theorem 3sstr4g 3511
Description: Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
Hypotheses
Ref Expression
3sstr4g.1
3sstr4g.2
3sstr4g.3
Assertion
Ref Expression
3sstr4g

Proof of Theorem 3sstr4g
StepHypRef Expression
1 3sstr4g.1 . 2
2 3sstr4g.2 . . 3
3 3sstr4g.3 . . 3
42, 3sseq12i 3496 . 2
51, 4sylibr 212 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1370  C_wss 3442
This theorem is referenced by:  rabss2  3549  unss2  3641  sslin  3690  ssopab2  4731  xpss12  5062  coss1  5112  coss2  5113  cnvss  5129  rnss  5185  ssres  5253  ssres2  5254  imass1  5322  imass2  5323  ssoprab2  6274  suppssfvOLD  6449  suppssov1OLD  6450  ressuppss  6842  tposss  6880  onovuni  6937  ss2ixp  7410  fodomfi  7725  cantnfp1lem3OLD  8051  isumsplit  13461  isumrpcl  13464  cvgrat  13501  gsumzf1o  16552  gsumzf1oOLD  16555  gsumzmhm  16592  gsumzmhmOLD  16593  gsumzinv  16604  gsumzinvOLD  16605  dsmmsubg  18361  divstgpopn  20089  metnrmlem2  20835  ovolsslem  21366  uniioombllem3  21465  ulmres  22253  xrlimcnp  22762  pntlemq  23250  subgornss  24262  sspba  24594  shlej2i  25251  chpssati  26236  sitgclbn  27185  subfacp1lem6  27529  predpredss  28087  aomclem4  29870  bnj1408  32870  coss12d  36469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3449  df-ss 3456
  Copyright terms: Public domain W3C validator