| 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 4163 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)) | |
| 4 | 1, 2, 3 | mp2an 692 | 1 ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∪ cun 3949 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-un 3956 |
| This theorem is referenced by: indir 4286 difundir 4291 difindi 4292 dfsymdif3 4306 unrab 4315 rabun2 4324 elnelun 4393 dfif6 4528 dfif3 4540 dfif5 4542 symdif0 5085 symdifid 5087 unopab 5224 xpundi 5754 xpundir 5755 xpun 5759 dmun 5921 resundi 6011 resundir 6012 cnvun 6162 rnun 6165 imaundi 6169 imaundir 6170 dmtpop 6238 coundi 6267 coundir 6268 unidmrn 6299 dfdm2 6301 predun 6349 mptun 6714 partfun 6715 resasplit 6778 fresaun 6779 fresaunres2 6780 residpr 7163 fpr 7174 sbthlem5 9127 1sdomOLD 9285 djuassen 10219 fz0to3un2pr 13669 fz0to4untppr 13670 fz0to5un2tp 13671 fzo0to42pr 13792 hashgval 14372 hashinf 14374 relexpcnv 15074 bpoly3 16094 vdwlem6 17024 setsres 17215 lefld 18637 opsrtoslem1 22079 volun 25580 nosupcbv 27747 noinfcbv 27762 lrold 27935 addsval2 27996 addscut 28011 addsunif 28035 addsbday 28050 mulsval2 28137 muls01 28138 mulsproplem2 28143 mulsproplem3 28144 mulsproplem4 28145 mulscut 28158 mulsunif 28176 addsdilem1 28177 addsdilem2 28178 mulsasslem1 28189 mulsasslem2 28190 mulsunif2 28196 precsexlemcbv 28230 onaddscl 28286 onmulscl 28287 n0scut 28338 1p1e2s 28400 nohalf 28407 ex-dif 30442 ex-in 30444 ex-pw 30448 ex-xp 30455 ex-cnv 30456 ex-rn 30459 fzodif1 32794 indval2 32839 ordtprsuni 33918 sigaclfu2 34122 eulerpartgbij 34374 subfacp1lem1 35184 subfacp1lem5 35189 fmla1 35392 fixun 35910 refssfne 36359 onint1 36450 bj-pr1un 37004 bj-pr21val 37014 bj-pr2un 37018 bj-pr22val 37020 poimirlem16 37643 poimirlem19 37646 itg2addnclem2 37679 iblabsnclem 37690 redvmptabs 42390 df3o3 43327 rclexi 43628 rtrclex 43630 cnvrcl0 43638 dfrtrcl5 43642 dfrcl2 43687 dfrcl4 43689 iunrelexp0 43715 relexpiidm 43717 corclrcl 43720 relexp01min 43726 corcltrcl 43752 cotrclrcl 43755 frege131d 43777 rnfdmpr 47293 31prm 47584 |
| Copyright terms: Public domain | W3C validator |