Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > uneq12i | Structured version Visualization version Unicode version |
Description: Equality inference for the union of two classes. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
Ref | Expression |
---|---|
uneq1i.1 | |
uneq12i.2 |
Ref | Expression |
---|---|
uneq12i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uneq1i.1 | . 2 | |
2 | uneq12i.2 | . 2 | |
3 | uneq12 3762 | . 2 | |
4 | 1, 2, 3 | mp2an 708 | 1 |
Colors of variables: wff setvar class |
Syntax hints: 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: indir 3875 difundir 3880 difindi 3881 dfsymdif3 3893 unrab 3898 rabun2 3906 elnelun 3964 elnelunOLD 3966 dfif6 4089 dfif3 4100 dfif5 4102 symdif0 4597 symdifid 4599 unopab 4728 xpundi 5171 xpundir 5172 xpun 5176 dmun 5331 resundi 5410 resundir 5411 cnvun 5538 rnun 5541 imaundi 5545 imaundir 5546 dmtpop 5611 coundi 5636 coundir 5637 unidmrn 5665 dfdm2 5667 predun 5704 mptun 6025 resasplit 6074 fresaun 6075 fresaunres2 6076 residpr 6409 fpr 6421 fvsnun2 6449 sbthlem5 8074 1sdom 8163 cdaassen 9004 fz0to3un2pr 12441 fz0to4untppr 12442 fzo0to42pr 12555 hashgval 13120 hashinf 13122 relexpcnv 13775 bpoly3 14789 vdwlem6 15690 setsres 15901 xpsc 16217 lefld 17226 opsrtoslem1 19484 volun 23313 iblcnlem1 23554 ex-dif 27280 ex-in 27282 ex-pw 27286 ex-xp 27293 ex-cnv 27294 ex-rn 27297 partfun 29475 ordtprsuni 29965 indval2 30076 sigaclfu2 30184 eulerpartgbij 30434 subfacp1lem1 31161 subfacp1lem5 31166 fixun 32016 refssfne 32353 onint1 32448 bj-pr1un 32991 bj-pr21val 33001 bj-pr2un 33005 bj-pr22val 33007 poimirlem16 33425 poimirlem19 33428 itg2addnclem2 33462 iblabsnclem 33473 rclexi 37922 rtrclex 37924 cnvrcl0 37932 dfrtrcl5 37936 dfrcl2 37966 dfrcl4 37968 iunrelexp0 37994 relexpiidm 37996 corclrcl 37999 relexp01min 38005 corcltrcl 38031 cotrclrcl 38034 frege131d 38056 df3o3 38323 rnfdmpr 41300 31prm 41512 |
Copyright terms: Public domain | W3C validator |