Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > uneq1d | Structured version Visualization version Unicode version |
Description: Deduction adding union to the right in a class equality. (Contributed by NM, 29-Mar-1998.) |
Ref | Expression |
---|---|
uneq1d.1 |
Ref | Expression |
---|---|
uneq1d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uneq1d.1 | . 2 | |
2 | uneq1 3760 | . 2 | |
3 | 1, 2 | syl 17 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1483 cun 3572 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-un 3579 |
This theorem is referenced by: ifeq1 4090 preq1 4268 tpeq1 4277 tpeq2 4278 tpprceq3 4335 iunxdif3 4606 iununi 4610 resasplit 6074 fresaunres2 6076 fmptpr 6438 funresdfunsn 6455 ressuppssdif 7316 sbthlem5 8074 fodomr 8111 domunfican 8233 brwdom2 8478 cdaval 8992 ackbij1lem2 9043 ttukeylem3 9333 snunioo 12298 snunioc 12300 prunioo 12301 fzpred 12389 fseq1p1m1 12414 nn0split 12454 fz0sn0fz1 12456 fzo0sn0fzo1 12557 fzosplitpr 12577 s2prop 13652 s4prop 13655 fsum1p 14482 fprod1p 14698 setsval 15888 setsabs 15902 setscom 15903 prdsval 16115 prdsdsval 16138 prdsdsval2 16144 prdsdsval3 16145 mreexexlem3d 16306 mreexexlem4d 16307 estrres 16779 symg2bas 17818 evlseu 19516 ordtuni 20994 lfinun 21328 alexsubALTlem3 21853 ustssco 22018 trust 22033 ressprdsds 22176 xpsdsval 22186 nulmbl2 23304 uniioombllem3 23353 uniioombllem4 23354 plyeq0 23967 plyaddlem1 23969 plymullem1 23970 fta1lem 24062 vieta1lem2 24066 birthdaylem2 24679 edglnl 26038 iuninc 29379 difelcarsg 30372 actfunsnf1o 30682 reprsuc 30693 breprexplema 30708 bnj1416 31107 mclsval 31460 mclsax 31466 rankung 32273 topjoin 32360 bj-tageq 32964 finixpnum 33394 poimirlem3 33412 poimirlem4 33413 poimirlem6 33415 poimirlem7 33416 poimirlem9 33418 poimirlem16 33425 poimirlem17 33426 poimirlem28 33437 mblfinlem2 33447 islshpsm 34267 lshpnel2N 34272 lkrlsp3 34391 pclfinclN 35236 dochsatshp 36740 mapfzcons1 37280 iunrelexp0 37994 isotone1 38346 fiiuncl 39234 nnsplit 39574 fourierdlem32 40356 fzopred 41332 fzopredsuc 41333 aacllem 42547 |
Copyright terms: Public domain | W3C validator |