![]() |
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 4157 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)) | |
4 | 1, 2, 3 | mp2an 690 | 1 ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 ∪ cun 3944 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-v 3463 df-un 3951 |
This theorem is referenced by: indir 4276 difundir 4281 difindi 4282 dfsymdif3 4297 unrab 4306 rabun2 4315 elnelun 4393 dfif6 4535 dfif3 4546 dfif5 4548 symdif0 5092 symdifid 5094 unopab 5234 xpundi 5749 xpundir 5750 xpun 5754 dmun 5916 resundi 6002 resundir 6003 cnvun 6153 rnun 6156 imaundi 6160 imaundir 6161 dmtpop 6228 coundi 6257 coundir 6258 unidmrn 6289 dfdm2 6291 predun 6340 mptun 6706 partfun 6707 resasplit 6771 fresaun 6772 fresaunres2 6773 residpr 7156 fpr 7167 sbthlem5 9124 1sdomOLD 9286 djuassen 10217 fz0to3un2pr 13652 fz0to4untppr 13653 fzo0to42pr 13768 hashgval 14345 hashinf 14347 relexpcnv 15035 bpoly3 16055 vdwlem6 16983 setsres 17175 lefld 18612 opsrtoslem1 22060 volun 25557 nosupcbv 27724 noinfcbv 27739 lrold 27912 addsval2 27969 addscut 27984 addsunif 28008 mulsval2 28104 muls01 28105 mulsproplem2 28110 mulsproplem3 28111 mulsproplem4 28112 mulscut 28125 mulsunif 28143 addsdilem1 28144 addsdilem2 28145 mulsasslem1 28156 mulsasslem2 28157 mulsunif2 28163 precsexlemcbv 28197 n0scut 28298 ex-dif 30348 ex-in 30350 ex-pw 30354 ex-xp 30361 ex-cnv 30362 ex-rn 30365 fzodif1 32684 ordtprsuni 33702 indval2 33815 sigaclfu2 33922 eulerpartgbij 34174 subfacp1lem1 34971 subfacp1lem5 34976 fmla1 35179 fixun 35693 refssfne 36030 onint1 36121 bj-pr1un 36670 bj-pr21val 36680 bj-pr2un 36684 bj-pr22val 36686 poimirlem16 37297 poimirlem19 37300 itg2addnclem2 37333 iblabsnclem 37344 df3o3 42929 rclexi 43231 rtrclex 43233 cnvrcl0 43241 dfrtrcl5 43245 dfrcl2 43290 dfrcl4 43292 iunrelexp0 43318 relexpiidm 43320 corclrcl 43323 relexp01min 43329 corcltrcl 43355 cotrclrcl 43358 frege131d 43380 rnfdmpr 46843 31prm 47118 |
Copyright terms: Public domain | W3C validator |