![]() |
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 3985 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)) | |
4 | 1, 2, 3 | mp2an 682 | 1 ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1601 ∪ cun 3790 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-v 3400 df-un 3797 |
This theorem is referenced by: indir 4102 difundir 4107 difindi 4108 dfsymdif3 4119 unrab 4124 rabun2 4132 elnelun 4192 dfif6 4310 dfif3 4321 dfif5 4323 symdif0 4832 symdifid 4834 unopab 4966 xpundi 5419 xpundir 5420 xpun 5424 dmun 5578 resundi 5662 resundir 5663 cnvun 5794 rnun 5797 imaundi 5801 imaundir 5802 dmtpop 5867 coundi 5892 coundir 5893 unidmrn 5921 dfdm2 5923 predun 5959 mptun 6273 resasplit 6326 fresaun 6327 fresaunres2 6328 residpr 6676 fpr 6689 fvsnun2OLD 6722 sbthlem5 8364 1sdom 8453 cdaassen 9341 fz0to3un2pr 12764 fz0to4untppr 12765 fzo0to42pr 12878 hashgval 13442 hashinf 13444 relexpcnv 14186 bpoly3 15195 vdwlem6 16098 setsres 16301 xpsc 16607 lefld 17616 opsrtoslem1 19884 volun 23753 iblcnlem1 23995 ex-dif 27859 ex-in 27861 ex-pw 27865 ex-xp 27872 ex-cnv 27873 ex-rn 27876 partfun 30045 ordtprsuni 30567 indval2 30678 sigaclfu2 30786 eulerpartgbij 31036 subfacp1lem1 31764 subfacp1lem5 31769 fixun 32609 refssfne 32945 onint1 33035 bj-pr1un 33567 bj-pr21val 33577 bj-pr2un 33581 bj-pr22val 33583 poimirlem16 34056 poimirlem19 34059 itg2addnclem2 34092 iblabsnclem 34103 rclexi 38889 rtrclex 38891 cnvrcl0 38899 dfrtrcl5 38903 dfrcl2 38933 dfrcl4 38935 iunrelexp0 38961 relexpiidm 38963 corclrcl 38966 relexp01min 38972 corcltrcl 38998 cotrclrcl 39001 frege131d 39023 df3o3 39289 rnfdmpr 42332 31prm 42543 |
Copyright terms: Public domain | W3C validator |