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 2627 | . . 3 | |
2 | 1 | abbidv 2257 | . 2 |
3 | dfuni2 3738 | . 2 | |
4 | dfuni2 3738 | . 2 | |
5 | 2, 3, 4 | 3eqtr4g 2197 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1331 cab 2125 wrex 2417 cuni 3736 |
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 2121 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-rex 2422 df-uni 3737 |
This theorem is referenced by: unieqi 3746 unieqd 3747 uniintsnr 3807 iununir 3896 treq 4032 limeq 4299 uniex 4359 uniexg 4361 ordsucunielexmid 4446 onsucuni2 4479 nnpredcl 4536 elvvuni 4603 unielrel 5066 unixp0im 5075 iotass 5105 nnsucuniel 6391 en1bg 6694 omp1eom 6980 ctmlemr 6993 uniopn 12168 istopon 12180 eltg3 12226 tgdom 12241 cldval 12268 ntrfval 12269 clsfval 12270 neifval 12309 tgrest 12338 cnprcl2k 12375 bj-uniex 13115 bj-uniexg 13116 nnsf 13199 peano3nninf 13201 exmidsbthr 13218 |
Copyright terms: Public domain | W3C validator |