![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > elun1 | Structured version Unicode version |
Description: Membership law for union of classes. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
elun1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssun1 3622 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | sseli 3455 |
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 1954 ax-ext 2431 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2602 df-v 3074 df-un 3436 df-in 3438 df-ss 3445 |
This theorem is referenced by: brtpos 6859 dftpos4 6869 domunsncan 7516 unxpdomlem2 7624 rankunb 8163 rankelun 8185 fin1a2lem10 8684 zornn0g 8780 xrsupexmnf 11373 xrinfmexpnf 11374 sumsplit 13348 prmreclem5 14094 lbsextlem3 17359 restntr 18913 1stckgenlem 19253 fbun 19540 filcon 19583 filuni 19585 alexsubALTlem4 19749 ovolfiniun 21111 volfiniun 21156 elplyd 21798 ply1term 21800 aannenlem2 21923 aalioulem2 21927 eengbas 23374 ecgrtg 23376 vdgrf 23715 altxpsspw 28147 mbfresfi 28581 itg2addnclem2 28587 ftc1anclem7 28616 ftc1anc 28618 comppfsc 28722 sucidALTVD 31919 sucidALT 31920 bnj1498 32365 hdmaplem1 35735 hdmap1eulem 35788 |
Copyright terms: Public domain | W3C validator |