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 4838 | . 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∪ 𝐴 = ∪ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ∪ cuni 4830 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-rex 3141 df-uni 4831 |
This theorem is referenced by: elunirab 4842 unisng 4845 unidif0 5251 univ 5334 uniop 5396 dfiun3g 5828 op1sta 6075 op2nda 6078 dfdm2 6125 unixpid 6128 unisuc 6260 iotajust 6306 dfiota2 6308 cbviotaw 6314 cbviota 6316 sb8iota 6318 dffv4 6660 funfv2f 6745 funiunfv 6998 elunirnALT 7002 riotauni 7109 ordunisuc 7536 1st0 7684 2nd0 7685 unielxp 7716 brtpos0 7888 dfrecs3 7998 recsfval 8006 tz7.44-3 8033 uniqs 8346 xpassen 8599 dffi3 8883 dfsup2 8896 sup00 8916 r1limg 9188 jech9.3 9231 rankxplim2 9297 rankxplim3 9298 rankxpsuc 9299 dfac5lem2 9538 kmlem11 9574 cflim2 9673 fin23lem30 9752 fin23lem34 9756 itunisuc 9829 itunitc 9831 ituniiun 9832 ac6num 9889 rankcf 10187 dprd2da 19093 dmdprdsplit2lem 19096 lssuni 19640 basdif0 21489 tgdif0 21528 neiptopuni 21666 restcls 21717 restntr 21718 pnrmopn 21879 cncmp 21928 discmp 21934 hauscmplem 21942 unisngl 22063 xkouni 22135 uptx 22161 ufildr 22467 ptcmplem3 22590 utop2nei 22786 utopreg 22788 zcld 23348 icccmp 23360 cncfcnvcn 23456 cnmpopc 23459 cnheibor 23486 evth 23490 evth2 23491 iunmbl 24081 voliun 24082 dvcnvrelem2 24542 ftc1 24566 aannenlem2 24845 circtopn 31000 locfinref 31004 tpr2rico 31054 cbvesum 31200 unibrsiga 31344 sxbrsigalem3 31429 dya2iocucvr 31441 sxbrsigalem1 31442 sibf0 31491 sibff 31493 sitgclg 31499 probfinmeasbALTV 31586 coinflipuniv 31638 cvmliftlem10 32438 dfon2lem7 32931 dfrdg2 32937 frrlem5 33024 frrlem8 33027 frrlem10 33029 noetalem4 33117 dfiota3 33281 dffv5 33282 dfrecs2 33308 dfrdg4 33309 ordcmp 33692 bj-nuliotaALT 34245 mptsnun 34502 finxp1o 34555 ftc1cnnc 34847 uniqsALTV 35467 cnvepima 35475 dfom6 39776 refsum2cnlem1 41171 lptre2pt 41797 limclner 41808 limclr 41812 stoweidlem62 42224 fourierdlem42 42311 fourierdlem80 42348 fouriercnp 42388 qndenserrn 42461 salexct3 42502 salgencntex 42503 salgensscntex 42504 subsalsal 42519 0ome 42688 borelmbl 42795 mbfresmf 42893 cnfsmf 42894 incsmf 42896 smfmbfcex 42913 decsmf 42920 smfpimbor1lem2 42951 setrec2 44726 |
Copyright terms: Public domain | W3C validator |