New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > sseq2 | Unicode version |
Description: Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.) |
Ref | Expression |
---|---|
sseq2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sstr2 3279 | . . . 4 | |
2 | 1 | com12 27 | . . 3 |
3 | sstr2 3279 | . . . 4 | |
4 | 3 | com12 27 | . . 3 |
5 | 2, 4 | anim12i 549 | . 2 |
6 | eqss 3287 | . 2 | |
7 | dfbi2 609 | . 2 | |
8 | 5, 6, 7 | 3imtr4i 257 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 176 wa 358 wceq 1642 wss 3257 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2478 df-v 2861 df-nin 3211 df-compl 3212 df-in 3213 df-ss 3259 |
This theorem is referenced by: sseq12 3294 sseq2i 3296 sseq2d 3299 syl5sseq 3319 nssne1 3327 psseq2 3357 sseq0 3582 un00 3586 disjpss 3601 pweq 3725 ssintab 3943 ssintub 3944 intmin 3946 p6eq 4238 opkelssetkg 4268 pw1equn 4331 pw1eqadj 4332 ssfin 4470 sfinltfin 4535 vfinspsslem1 4550 brssetg 4757 fununi 5160 funcnvuni 5161 feq3 5212 clos1induct 5880 frd 5922 nclec 6195 lecidg 6196 lecncvg 6199 ltcpw1pwg 6202 sbthlem2 6204 addlec 6208 nc0le1 6216 ce2le 6233 tlenc1c 6240 |
Copyright terms: Public domain | W3C validator |