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

Theorem 3sstr4g 2954
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 (φAB)
3sstr4g.2 𝐶 = A
3sstr4g.3 𝐷 = B
Assertion
Ref Expression
3sstr4g (φ𝐶𝐷)

Proof of Theorem 3sstr4g
StepHypRef Expression
1 3sstr4g.1 . 2 (φAB)
2 3sstr4g.2 . . 3 𝐶 = A
3 3sstr4g.3 . . 3 𝐷 = B
42, 3sseq12i 2939 . 2 (𝐶𝐷AB)
51, 4sylibr 137 1 (φ𝐶𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1223  wss 2885
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 1309  ax-7 1310  ax-gen 1311  ax-ie1 1355  ax-ie2 1356  ax-8 1368  ax-11 1370  ax-4 1373  ax-17 1392  ax-i9 1396  ax-ial 1400  ax-i5r 1401  ax-ext 1995
This theorem depends on definitions:  df-bi 110  df-nf 1323  df-sb 1619  df-clab 2000  df-cleq 2006  df-clel 2009  df-in 2892  df-ss 2899
This theorem is referenced by:  rabss2  2991  unss2  3082  sslin  3131  ssopab2  3975  xpss12  4360  coss1  4406  coss2  4407  cnvss  4423  rnss  4479  ssres  4552  ssres2  4553  imass1  4615  imass2  4616  imadif  4893  imain  4895  ssoprab2  5472  suppssfv  5619  suppssov1  5620  tposss  5771
  Copyright terms: Public domain W3C validator