![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssequn2 | Structured version Visualization version Unicode version |
Description: A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.) |
Ref | Expression |
---|---|
ssequn2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssequn1 3616 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | uncom 3590 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | eqeq1i 2467 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | bitri 257 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-v 3059 df-un 3421 df-in 3423 df-ss 3430 |
This theorem is referenced by: unabs 3685 tppreqb 4126 pwssun 4759 pwundif 4760 relresfld 5381 relcoi1OLD 5384 ordssun 5541 ordequn 5542 oneluni 5554 fsnunf 6126 sorpssun 6605 ordunpr 6680 fodomr 7749 enp1ilem 7831 pwfilem 7894 brwdom2 8114 sucprcreg 8140 dfacfin7 8855 hashbclem 12648 incexclem 13943 ramub1lem1 15033 ramub1lem2 15034 mreexmrid 15598 lspun0 18283 lbsextlem4 18433 cldlp 20215 ordtuni 20255 lfinun 20589 cldsubg 21174 trust 21293 nulmbl2 22539 limcmpt2 22888 cnplimc 22891 dvreslem 22913 dvaddbr 22941 dvmulbr 22942 lhop 23017 plypf1 23215 coeeulem 23227 coeeu 23228 coef2 23234 rlimcnp 23940 ex-un 25923 shs0i 27151 chj0i 27157 disjun0 28254 ffsrn 28363 difioo 28413 eulerpartlemt 29253 subfacp1lem1 29951 cvmscld 30045 mthmpps 30269 refssfne 31063 topjoin 31070 poimirlem3 31988 poimirlem28 32013 rntrclfvOAI 35578 istopclsd 35587 nacsfix 35599 diophrw 35646 clcnvlem 36275 cnvrcl0 36277 dmtrcl 36279 rntrcl 36280 iunrelexp0 36339 dmtrclfvRP 36367 rntrclfv 36369 cotrclrcl 36379 limciccioolb 37739 limcicciooub 37755 ioccncflimc 37801 icocncflimc 37805 stoweidlem44 37943 dirkercncflem3 38005 fourierdlem62 38070 ismeannd 38343 |
Copyright terms: Public domain | W3C validator |