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 4804 | . 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∪ 𝐴 = ∪ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ∪ cuni 4793 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-v 3399 df-in 3848 df-ss 3858 df-uni 4794 |
This theorem is referenced by: elunirab 4809 unisng 4814 unidif0 5223 univ 5307 uniop 5369 dfiun3g 5801 op1sta 6051 op2nda 6054 dfdm2 6107 unixpid 6110 unisuc 6242 iotajust 6290 dfiota2 6292 cbviotaw 6298 cbviotavw 6299 cbviota 6301 sb8iota 6303 dffv4 6665 funfv2f 6751 funiunfv 7012 elunirnALT 7016 riotauni 7127 ordunisuc 7560 1st0 7713 2nd0 7714 unielxp 7745 brtpos0 7921 dfrecs3 8031 recsfval 8039 tz7.44-3 8066 uniqs 8381 xpassen 8653 dffi3 8961 dfsup2 8974 sup00 8994 r1limg 9266 jech9.3 9309 rankxplim2 9375 rankxplim3 9376 rankxpsuc 9377 dfac5lem2 9617 kmlem11 9653 cflim2 9756 fin23lem30 9835 fin23lem34 9839 itunisuc 9912 itunitc 9914 ituniiun 9915 ac6num 9972 rankcf 10270 dprd2da 19276 dmdprdsplit2lem 19279 lssuni 19823 basdif0 21697 tgdif0 21736 neiptopuni 21874 restcls 21925 restntr 21926 pnrmopn 22087 cncmp 22136 discmp 22142 hauscmplem 22150 unisngl 22271 xkouni 22343 uptx 22369 ufildr 22675 ptcmplem3 22798 utop2nei 22995 utopreg 22997 zcld 23558 icccmp 23570 cncfcnvcn 23670 cnmpopc 23673 cnheibor 23700 evth 23704 evth2 23705 iunmbl 24298 voliun 24299 dvcnvrelem2 24762 ftc1 24786 aannenlem2 25069 circtopn 31351 locfinref 31355 zarmxt1 31394 tpr2rico 31426 cbvesum 31572 unibrsiga 31716 sxbrsigalem3 31801 dya2iocucvr 31813 sxbrsigalem1 31814 sibf0 31863 sibff 31865 sitgclg 31871 probfinmeasbALTV 31958 coinflipuniv 32010 cvmliftlem10 32819 dfon2lem7 33329 dfrdg2 33335 frrlem5 33437 frrlem8 33440 frrlem10 33442 bday1s 33658 old0 33686 made0 33687 madeoldsuc 33697 dfiota3 33855 dffv5 33856 dfrecs2 33882 dfrdg4 33883 ordcmp 34266 bj-nuliotaALT 34841 mptsnun 35122 finxp1o 35175 ftc1cnnc 35461 uniqsALTV 36076 cnvepima 36084 dfom6 40676 refsum2cnlem1 42102 lptre2pt 42707 limclner 42718 limclr 42722 stoweidlem62 43129 fourierdlem42 43216 fourierdlem80 43253 fouriercnp 43293 qndenserrn 43366 salexct3 43407 salgencntex 43408 salgensscntex 43409 subsalsal 43424 0ome 43593 borelmbl 43700 mbfresmf 43798 cnfsmf 43799 incsmf 43801 smfmbfcex 43818 decsmf 43825 smfpimbor1lem2 43856 setrec2 45838 |
Copyright terms: Public domain | W3C validator |