![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > uneq12i | Structured version Visualization version GIF 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 3897 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)) | |
4 | 1, 2, 3 | mp2an 710 | 1 ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1624 ∪ cun 3705 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-v 3334 df-un 3712 |
This theorem is referenced by: indir 4010 difundir 4015 difindi 4016 dfsymdif3 4028 unrab 4033 rabun2 4041 elnelun 4099 elnelunOLD 4101 dfif6 4225 dfif3 4236 dfif5 4238 symdif0 4741 symdifid 4743 unopab 4872 xpundi 5320 xpundir 5321 xpun 5325 dmun 5478 resundi 5560 resundir 5561 cnvun 5688 rnun 5691 imaundi 5695 imaundir 5696 dmtpop 5762 coundi 5789 coundir 5790 unidmrn 5818 dfdm2 5820 predun 5857 mptun 6178 resasplit 6227 fresaun 6228 fresaunres2 6229 residpr 6564 fpr 6576 fvsnun2 6605 sbthlem5 8231 1sdom 8320 cdaassen 9188 fz0to3un2pr 12627 fz0to4untppr 12628 fzo0to42pr 12741 hashgval 13306 hashinf 13308 relexpcnv 13966 bpoly3 14980 vdwlem6 15884 setsres 16095 xpsc 16411 lefld 17419 opsrtoslem1 19678 volun 23505 iblcnlem1 23745 ex-dif 27583 ex-in 27585 ex-pw 27589 ex-xp 27596 ex-cnv 27597 ex-rn 27600 partfun 29776 ordtprsuni 30266 indval2 30377 sigaclfu2 30485 eulerpartgbij 30735 subfacp1lem1 31460 subfacp1lem5 31465 fixun 32314 refssfne 32651 onint1 32746 bj-pr1un 33289 bj-pr21val 33299 bj-pr2un 33303 bj-pr22val 33305 poimirlem16 33730 poimirlem19 33733 itg2addnclem2 33767 iblabsnclem 33778 rclexi 38416 rtrclex 38418 cnvrcl0 38426 dfrtrcl5 38430 dfrcl2 38460 dfrcl4 38462 iunrelexp0 38488 relexpiidm 38490 corclrcl 38493 relexp01min 38499 corcltrcl 38525 cotrclrcl 38528 frege131d 38550 df3o3 38817 rnfdmpr 41800 31prm 42014 |
Copyright terms: Public domain | W3C validator |