Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > uneq2 | Structured version Visualization version Unicode version |
Description: Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
uneq2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uneq1 3760 | . 2 | |
2 | uncom 3757 | . 2 | |
3 | uncom 3757 | . 2 | |
4 | 1, 2, 3 | 3eqtr4g 2681 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1483 cun 3572 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-un 3579 |
This theorem is referenced by: uneq12 3762 uneq2i 3764 uneq2d 3767 uneqin 3878 disjssun 4036 uniprg 4450 unexb 6958 undifixp 7944 unxpdom 8167 ackbij1lem16 9057 fin23lem28 9162 ttukeylem6 9336 lcmfun 15358 ipodrsima 17165 mplsubglem 19434 mretopd 20896 iscldtop 20899 dfconn2 21222 nconnsubb 21226 comppfsc 21335 spanun 28404 locfinref 29908 isros 30231 unelros 30234 difelros 30235 rossros 30243 inelcarsg 30373 noextendseq 31820 rankung 32273 paddval 35084 dochsatshp 36740 nacsfix 37275 eldioph4b 37375 eldioph4i 37376 fiuneneq 37775 isotone1 38346 fiiuncl 39234 |
Copyright terms: Public domain | W3C validator |