![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > 3sstr4i | Structured version Unicode version |
Description: Substitution of equality in both sides of a subclass relationship. (Contributed by NM, 13-Jan-1996.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
Ref | Expression |
---|---|
3sstr4.1 |
![]() ![]() ![]() ![]() |
3sstr4.2 |
![]() ![]() ![]() ![]() |
3sstr4.3 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3sstr4i |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3sstr4.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | 3sstr4.2 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 3sstr4.3 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 2, 3 | sseq12i 3493 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | mpbir 209 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
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 3446 df-ss 3453 |
This theorem is referenced by: brab2a 4999 rncoss 5211 imassrn 5291 rnin 5357 inimass 5364 ssoprab2i 6292 omopthlem2 7208 rankval4 8188 cardf2 8227 r0weon 8293 dcomex 8730 axdc2lem 8731 fpwwe2lem1 8912 canthwe 8932 recmulnq 9247 npex 9269 axresscn 9429 odlem1 16162 gexlem1 16202 psrbagsn 17704 bwth 19148 2ndcctbss 19194 uniioombllem4 21202 uniioombllem5 21203 eff1olem 22140 birthdaylem1 22481 nvss 24143 lediri 25112 lejdiri 25114 sshhococi 25121 mayetes3i 25305 disjxpin 26101 imadifxp 26110 sxbrsigalem5 26867 eulerpartlemmf 26922 kur14lem6 27263 cvmlift2lem12 27367 bpoly4 28366 mblfinlem4 28599 areaquad 29760 relopabVD 31989 bj-rrhatsscchat 32917 lclkrs2 35543 |
Copyright terms: Public domain | W3C validator |