![]() |
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 3990 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)) | |
4 | 1, 2, 3 | mp2an 685 | 1 ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1658 ∪ cun 3797 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-ext 2804 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-v 3417 df-un 3804 |
This theorem is referenced by: indir 4106 difundir 4111 difindi 4112 dfsymdif3 4123 unrab 4128 rabun2 4136 elnelun 4192 dfif6 4310 dfif3 4321 dfif5 4323 symdif0 4818 symdifid 4820 unopab 4952 xpundi 5405 xpundir 5406 xpun 5410 dmun 5564 resundi 5648 resundir 5649 cnvun 5780 rnun 5783 imaundi 5787 imaundir 5788 dmtpop 5853 coundi 5878 coundir 5879 unidmrn 5907 dfdm2 5909 predun 5945 mptun 6259 resasplit 6312 fresaun 6313 fresaunres2 6314 residpr 6660 fpr 6673 fvsnun2OLD 6706 sbthlem5 8344 1sdom 8433 cdaassen 9320 fz0to3un2pr 12737 fz0to4untppr 12738 fzo0to42pr 12851 hashgval 13414 hashinf 13416 relexpcnv 14153 bpoly3 15162 vdwlem6 16062 setsres 16265 xpsc 16571 lefld 17580 opsrtoslem1 19845 volun 23712 iblcnlem1 23954 ex-dif 27839 ex-in 27841 ex-pw 27845 ex-xp 27852 ex-cnv 27853 ex-rn 27856 partfun 30024 ordtprsuni 30511 indval2 30622 sigaclfu2 30730 eulerpartgbij 30980 subfacp1lem1 31708 subfacp1lem5 31713 fixun 32556 refssfne 32892 onint1 32982 bj-pr1un 33514 bj-pr21val 33524 bj-pr2un 33528 bj-pr22val 33530 poimirlem16 33970 poimirlem19 33973 itg2addnclem2 34006 iblabsnclem 34017 rclexi 38764 rtrclex 38766 cnvrcl0 38774 dfrtrcl5 38778 dfrcl2 38808 dfrcl4 38810 iunrelexp0 38836 relexpiidm 38838 corclrcl 38841 relexp01min 38847 corcltrcl 38873 cotrclrcl 38876 frege131d 38898 df3o3 39164 rnfdmpr 42185 31prm 42343 |
Copyright terms: Public domain | W3C validator |