![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > unieqi | Structured version Visualization version Unicode 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 4220 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-rex 2755 df-uni 4213 |
This theorem is referenced by: elunirab 4224 unisn 4227 unidif0 4590 univ 4665 uniop 4718 dfiun3g 5106 op1sta 5337 op2nda 5340 dfdm2 5387 unixpid 5390 unisuc 5518 iotajust 5564 dfiota2 5566 cbviota 5570 sb8iota 5572 dffv4 5885 funfv2f 5957 funiunfv 6178 elunirnALT 6182 riotauni 6283 ordunisuc 6686 1st0 6826 2nd0 6827 unielxp 6856 brtpos0 7006 dfrecs3 7117 recsfval 7125 tz7.44-3 7152 uniqs 7449 xpassen 7692 dffi3 7971 dfsup2 7984 sup00 8004 r1limg 8268 jech9.3 8311 rankxplim2 8377 rankxplim3 8378 rankxpsuc 8379 dfac5lem2 8581 kmlem11 8616 cflim2 8719 fin23lem30 8798 fin23lem34 8802 itunisuc 8875 itunitc 8877 ituniiun 8878 ac6num 8935 rankcf 9228 dprd2da 17724 dmdprdsplit2lem 17727 lssuni 18212 basdif0 20017 tgdif0 20057 neiptopuni 20195 restcls 20246 restntr 20247 pnrmopn 20408 cncmp 20456 discmp 20462 hauscmplem 20470 unisngl 20591 xkouni 20663 uptx 20689 ufildr 20995 ptcmplem3 21118 utop2nei 21314 utopreg 21316 zcld 21880 icccmp 21892 cncfcnvcn 22002 cnmpt2pc 22005 cnheibor 22032 evth 22036 evth2 22037 iunmbl 22555 voliun 22556 dvcnvrelem2 23019 ftc1 23043 aannenlem2 23334 circtopn 28713 locfinref 28717 tpr2rico 28767 cbvesum 28912 unibrsiga 29057 sxbrsigalem3 29143 dya2iocucvr 29155 sxbrsigalem1 29156 sibf0 29216 sibff 29218 sitgclg 29224 probfinmeasbOLD 29310 coinflipuniv 29363 cvmliftlem10 30066 dfon2lem7 30484 dfrdg2 30491 frrlem11 30575 dfiota3 30739 dffv5 30740 dfrecs2 30766 dfrdg4 30767 ordcmp 31156 bj-nuliotaALT 31669 mptsnun 31786 finxp1o 31829 ftc1cnnc 32061 refsum2cnlem1 37398 lptre2pt 37758 limclner 37770 limclr 37774 stoweidlem62 37961 stoweidlem62OLD 37962 fourierdlem42 38050 fourierdlem42OLD 38051 fourierdlem80 38088 fouriercnp 38128 qndenserrn 38206 salexct3 38239 salgencntex 38240 salgensscntex 38241 0ome 38388 borelmbl 38496 |
Copyright terms: Public domain | W3C validator |