![]() |
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 4918 | . 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∪ 𝐴 = ∪ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ∪ cuni 4907 |
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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-in 3954 df-ss 3964 df-uni 4908 |
This theorem is referenced by: elunirab 4923 unisng 4928 unidif0 5357 univ 5450 uniop 5514 dfiun3g 5961 op1sta 6221 op2nda 6224 dfdm2 6277 unixpid 6280 unisucs 6438 iotajust 6491 dfiota2 6493 cbviotaw 6499 cbviotavw 6500 cbviota 6502 sb8iota 6504 dffv4 6885 funfv2f 6976 funiunfv 7242 elunirnALT 7246 riotauni 7366 ordunisuc 7815 1st0 7976 2nd0 7977 unielxp 8008 brtpos0 8213 frrlem5 8270 frrlem8 8273 frrlem10 8275 dfwrecsOLD 8293 dfrecs3 8367 dfrecs3OLD 8368 recsfval 8376 tz7.44-3 8403 nlim1 8484 nlim2 8485 uniqs 8767 xpassen 9062 dffi3 9422 dfsup2 9435 sup00 9455 r1limg 9762 jech9.3 9805 rankxplim2 9871 rankxplim3 9872 rankxpsuc 9873 dfac5lem2 10115 kmlem11 10151 cflim2 10254 fin23lem30 10333 fin23lem34 10337 itunisuc 10410 itunitc 10412 ituniiun 10413 ac6num 10470 rankcf 10768 dprd2da 19904 dmdprdsplit2lem 19907 lssuni 20538 basdif0 22438 tgdif0 22477 neiptopuni 22616 restcls 22667 restntr 22668 pnrmopn 22829 cncmp 22878 discmp 22884 hauscmplem 22892 unisngl 23013 xkouni 23085 uptx 23111 ufildr 23417 ptcmplem3 23540 utop2nei 23737 utopreg 23739 zcld 24311 icccmp 24323 cncfcnvcn 24423 cnmpopc 24426 cnheibor 24453 evth 24457 evth2 24458 iunmbl 25052 voliun 25053 dvcnvrelem2 25517 ftc1 25541 aannenlem2 25824 bday1s 27312 old0 27334 made0 27348 old1 27350 madeoldsuc 27359 circtopn 32755 locfinref 32759 zarmxt1 32798 tpr2rico 32830 cbvesum 32978 unibrsiga 33122 sxbrsigalem3 33209 dya2iocucvr 33221 sxbrsigalem1 33222 sibf0 33271 sibff 33273 sitgclg 33279 probfinmeasbALTV 33366 coinflipuniv 33418 cvmliftlem10 34223 dfon2lem7 34699 dfrdg2 34705 dfiota3 34833 dffv5 34834 dfrecs2 34860 dfrdg4 34861 ordcmp 35270 bj-nuliotaALT 35877 mptsnun 36158 finxp1o 36211 ftc1cnnc 36498 uniqsALTV 37136 cnvepima 37144 sn-iotalemcor 40987 onsucunitp 42056 dfom6 42215 refsum2cnlem1 43654 lptre2pt 44291 limclner 44302 limclr 44306 stoweidlem62 44713 fourierdlem42 44800 fourierdlem80 44837 fouriercnp 44877 qndenserrn 44950 salexct3 44993 salgencntex 44994 salgensscntex 44995 subsalsal 45010 0ome 45180 borelmbl 45287 mbfresmf 45390 cnfsmf 45391 incsmf 45393 smfmbfcex 45411 decsmf 45418 smfpimbor1lem2 45450 ipoglb0 47521 setrec2 47642 |
Copyright terms: Public domain | W3C validator |