Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > unieq | Unicode version |
Description: Equality theorem for class union. Exercise 15 of [TakeutiZaring] p. 18. (Contributed by NM, 10-Aug-1993.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Ref | Expression |
---|---|
unieq |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexeq 2625 | . . 3 | |
2 | 1 | abbidv 2255 | . 2 |
3 | dfuni2 3733 | . 2 | |
4 | dfuni2 3733 | . 2 | |
5 | 2, 3, 4 | 3eqtr4g 2195 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1331 cab 2123 wrex 2415 cuni 3731 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-rex 2420 df-uni 3732 |
This theorem is referenced by: unieqi 3741 unieqd 3742 uniintsnr 3802 iununir 3891 treq 4027 limeq 4294 uniex 4354 uniexg 4356 ordsucunielexmid 4441 onsucuni2 4474 nnpredcl 4531 elvvuni 4598 unielrel 5061 unixp0im 5070 iotass 5100 nnsucuniel 6384 en1bg 6687 omp1eom 6973 ctmlemr 6986 uniopn 12157 istopon 12169 eltg3 12215 tgdom 12230 cldval 12257 ntrfval 12258 clsfval 12259 neifval 12298 tgrest 12327 cnprcl2k 12364 bj-uniex 13104 bj-uniexg 13105 nnsf 13188 peano3nninf 13190 exmidsbthr 13207 |
Copyright terms: Public domain | W3C validator |