Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > unieqi | Structured version Visualization version GIF version |
Description: Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993.) |
Ref | Expression |
---|---|
unieqi.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
unieqi | ⊢ ∪ 𝐴 = ∪ 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unieqi.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | unieq 4850 | . 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∪ 𝐴 = ∪ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 ∪ cuni 4839 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3434 df-in 3894 df-ss 3904 df-uni 4840 |
This theorem is referenced by: elunirab 4855 unisng 4860 unidif0 5282 univ 5367 uniop 5429 dfiun3g 5873 op1sta 6128 op2nda 6131 dfdm2 6184 unixpid 6187 unisuc 6342 iotajust 6390 dfiota2 6392 cbviotaw 6398 cbviotavw 6399 cbviota 6401 sb8iota 6403 dffv4 6771 funfv2f 6857 funiunfv 7121 elunirnALT 7125 riotauni 7238 ordunisuc 7679 1st0 7837 2nd0 7838 unielxp 7869 brtpos0 8049 frrlem5 8106 frrlem8 8109 frrlem10 8111 dfwrecsOLD 8129 dfrecs3 8203 dfrecs3OLD 8204 recsfval 8212 tz7.44-3 8239 nlim1 8319 nlim2 8320 uniqs 8566 xpassen 8853 dffi3 9190 dfsup2 9203 sup00 9223 r1limg 9529 jech9.3 9572 rankxplim2 9638 rankxplim3 9639 rankxpsuc 9640 dfac5lem2 9880 kmlem11 9916 cflim2 10019 fin23lem30 10098 fin23lem34 10102 itunisuc 10175 itunitc 10177 ituniiun 10178 ac6num 10235 rankcf 10533 dprd2da 19645 dmdprdsplit2lem 19648 lssuni 20201 basdif0 22103 tgdif0 22142 neiptopuni 22281 restcls 22332 restntr 22333 pnrmopn 22494 cncmp 22543 discmp 22549 hauscmplem 22557 unisngl 22678 xkouni 22750 uptx 22776 ufildr 23082 ptcmplem3 23205 utop2nei 23402 utopreg 23404 zcld 23976 icccmp 23988 cncfcnvcn 24088 cnmpopc 24091 cnheibor 24118 evth 24122 evth2 24123 iunmbl 24717 voliun 24718 dvcnvrelem2 25182 ftc1 25206 aannenlem2 25489 circtopn 31787 locfinref 31791 zarmxt1 31830 tpr2rico 31862 cbvesum 32010 unibrsiga 32154 sxbrsigalem3 32239 dya2iocucvr 32251 sxbrsigalem1 32252 sibf0 32301 sibff 32303 sitgclg 32309 probfinmeasbALTV 32396 coinflipuniv 32448 cvmliftlem10 33256 dfon2lem7 33765 dfrdg2 33771 bday1s 34025 old0 34043 made0 34057 madeoldsuc 34067 dfiota3 34225 dffv5 34226 dfrecs2 34252 dfrdg4 34253 ordcmp 34636 bj-nuliotaALT 35229 mptsnun 35510 finxp1o 35563 ftc1cnnc 35849 uniqsALTV 36464 cnvepima 36472 sn-iotalemcor 40190 nlimsuc 41048 dfom6 41138 refsum2cnlem1 42580 lptre2pt 43181 limclner 43192 limclr 43196 stoweidlem62 43603 fourierdlem42 43690 fourierdlem80 43727 fouriercnp 43767 qndenserrn 43840 salexct3 43881 salgencntex 43882 salgensscntex 43883 subsalsal 43898 0ome 44067 borelmbl 44174 mbfresmf 44275 cnfsmf 44276 incsmf 44278 smfmbfcex 44295 decsmf 44302 smfpimbor1lem2 44333 ipoglb0 46280 setrec2 46401 |
Copyright terms: Public domain | W3C validator |