| 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 1540 ∪ cuni 4907 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-uni 4908 |
| This theorem is referenced by: elunirab 4922 unisng 4925 unidif0 5360 univ 5456 uniop 5520 dfiun3g 5978 op1sta 6245 op2nda 6248 dfdm2 6301 unixpid 6304 unisucs 6461 iotajust 6513 dfiota2 6515 cbviotaw 6521 cbviotavw 6522 cbviota 6523 sb8iota 6525 dffv4 6903 funfv2f 6998 funiunfv 7268 elunirnALT 7272 riotauni 7394 ordunisuc 7852 1st0 8020 2nd0 8021 unielxp 8052 brtpos0 8258 frrlem5 8315 frrlem8 8318 frrlem10 8320 dfwrecsOLD 8338 dfrecs3 8412 dfrecs3OLD 8413 recsfval 8421 tz7.44-3 8448 nlim1 8527 nlim2 8528 uniqs 8817 xpassen 9106 dffi3 9471 dfsup2 9484 sup00 9504 r1limg 9811 jech9.3 9854 rankxplim2 9920 rankxplim3 9921 rankxpsuc 9922 dfac5lem2 10164 kmlem11 10201 cflim2 10303 fin23lem30 10382 fin23lem34 10386 itunisuc 10459 itunitc 10461 ituniiun 10462 ac6num 10519 rankcf 10817 dprd2da 20062 dmdprdsplit2lem 20065 lssuni 20937 basdif0 22960 tgdif0 22999 neiptopuni 23138 restcls 23189 restntr 23190 pnrmopn 23351 cncmp 23400 discmp 23406 hauscmplem 23414 unisngl 23535 xkouni 23607 uptx 23633 ufildr 23939 ptcmplem3 24062 utop2nei 24259 utopreg 24261 zcld 24835 icccmp 24847 cncfcnvcn 24952 cnmpopc 24955 cnheibor 24987 evth 24991 evth2 24992 iunmbl 25588 voliun 25589 dvcnvrelem2 26057 ftc1 26083 aannenlem2 26371 bday1s 27876 old0 27898 made0 27912 old1 27914 madeoldsuc 27923 zs12bday 28424 isconstr 33777 circtopn 33836 locfinref 33840 zarmxt1 33879 tpr2rico 33911 cbvesum 34043 cbvesumv 34044 unibrsiga 34187 sxbrsigalem3 34274 dya2iocucvr 34286 sxbrsigalem1 34287 sibf0 34336 sibff 34338 sitgclg 34344 probfinmeasbALTV 34431 coinflipuniv 34484 wevgblacfn 35114 cvmliftlem10 35299 dfon2lem7 35790 dfrdg2 35796 dfiota3 35924 dffv5 35925 dfrecs2 35951 dfrdg4 35952 ordcmp 36448 bj-nuliotaALT 37059 mptsnun 37340 finxp1o 37393 ftc1cnnc 37699 uniqsALTV 38330 cnvepima 38338 sn-iotalemcor 42261 onsucunitp 43386 dfom6 43544 refsum2cnlem1 45042 lptre2pt 45655 limclner 45666 limclr 45670 stoweidlem62 46077 fourierdlem42 46164 fourierdlem80 46201 fouriercnp 46241 qndenserrn 46314 salexct3 46357 salgencntex 46358 salgensscntex 46359 subsalsal 46374 0ome 46544 borelmbl 46651 mbfresmf 46754 cnfsmf 46755 incsmf 46757 smfmbfcex 46775 decsmf 46782 smfpimbor1lem2 46814 dftpos5 48774 ipoglb0 48883 setrec2 49214 |
| Copyright terms: Public domain | W3C validator |