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 4380 | . 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∪ 𝐴 = ∪ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 ∪ cuni 4372 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rex 2902 df-uni 4373 |
This theorem is referenced by: elunirab 4384 unisn 4387 unidif0 4764 univ 4846 uniop 4902 dfiun3g 5299 op1sta 5535 op2nda 5538 dfdm2 5584 unixpid 5587 unisuc 5718 iotajust 5767 dfiota2 5769 cbviota 5773 sb8iota 5775 dffv4 6100 funfv2f 6177 funiunfv 6410 elunirnALT 6414 riotauni 6517 ordunisuc 6924 1st0 7065 2nd0 7066 unielxp 7095 brtpos0 7246 dfrecs3 7356 recsfval 7364 tz7.44-3 7391 uniqs 7694 xpassen 7939 dffi3 8220 dfsup2 8233 sup00 8253 r1limg 8517 jech9.3 8560 rankxplim2 8626 rankxplim3 8627 rankxpsuc 8628 dfac5lem2 8830 kmlem11 8865 cflim2 8968 fin23lem30 9047 fin23lem34 9051 itunisuc 9124 itunitc 9126 ituniiun 9127 ac6num 9184 rankcf 9478 dprd2da 18264 dmdprdsplit2lem 18267 lssuni 18761 basdif0 20568 tgdif0 20607 neiptopuni 20744 restcls 20795 restntr 20796 pnrmopn 20957 cncmp 21005 discmp 21011 hauscmplem 21019 unisngl 21140 xkouni 21212 uptx 21238 ufildr 21545 ptcmplem3 21668 utop2nei 21864 utopreg 21866 zcld 22424 icccmp 22436 cncfcnvcn 22532 cnmpt2pc 22535 cnheibor 22562 evth 22566 evth2 22567 iunmbl 23128 voliun 23129 dvcnvrelem2 23585 ftc1 23609 aannenlem2 23888 circtopn 29232 locfinref 29236 tpr2rico 29286 cbvesum 29431 unibrsiga 29576 sxbrsigalem3 29661 dya2iocucvr 29673 sxbrsigalem1 29674 sibf0 29723 sibff 29725 sitgclg 29731 probfinmeasbOLD 29817 coinflipuniv 29870 cvmliftlem10 30530 dfon2lem7 30938 dfrdg2 30945 frrlem11 31036 dfiota3 31200 dffv5 31201 dfrecs2 31227 dfrdg4 31228 ordcmp 31616 bj-nuliotaALT 32211 mptsnun 32362 finxp1o 32405 ftc1cnnc 32654 refsum2cnlem1 38219 lptre2pt 38707 limclner 38718 limclr 38722 stoweidlem62 38955 fourierdlem42 39042 fourierdlem80 39079 fouriercnp 39119 qndenserrn 39195 salexct3 39236 salgencntex 39237 salgensscntex 39238 subsalsal 39253 0ome 39419 borelmbl 39526 mbfresmf 39626 cnfsmf 39627 incsmf 39629 smfmbfcex 39646 decsmf 39653 smfpimbor1lem2 39684 setrec2 42241 |
Copyright terms: Public domain | W3C validator |