![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > uneq1i | Structured version Visualization version GIF version |
Description: Inference adding union to the right in a class equality. (Contributed by NM, 30-Aug-1993.) |
Ref | Expression |
---|---|
uneq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
uneq1i | ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uneq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | uneq1 4152 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 ∪ cun 3942 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2698 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-v 3471 df-un 3949 |
This theorem is referenced by: un12 4163 unundi 4166 undif1 4471 dfif5 4540 tpcoma 4750 qdass 4753 qdassr 4754 tpidm12 4755 symdifv 5083 unidif0 5354 cnvimassrndm 6150 difxp2 6164 resasplit 6761 fresaun 6762 fresaunres2 6763 f1ofvswap 7309 df2o3 8488 sbthlem6 9106 fodomr 9146 domss2 9154 domunfican 9338 kmlem11 10177 hashfun 14422 prmreclem2 16879 setscom 17142 gsummptfzsplitl 19881 dfcnfldOLD 21288 uniioombllem3 25507 lhop 25942 sltlpss 27826 slelss 27827 addsasslem1 27913 mulsproplem5 28013 mulsproplem6 28014 mulsproplem7 28015 mulsproplem8 28016 ex-un 30227 ex-pw 30232 indifundif 32314 cycpmrn 32858 bnj1415 34659 subfacp1lem1 34779 lineunray 35733 bj-2upln1upl 36493 poimirlem3 37085 poimirlem4 37086 poimirlem5 37087 poimirlem16 37098 poimirlem17 37099 poimirlem19 37101 poimirlem20 37102 poimirlem22 37104 metakunt24 41652 df3o2 42714 omcl3g 42735 dfrcl2 43076 iunrelexp0 43104 trclfvdecomr 43130 corcltrcl 43141 cotrclrcl 43144 fourierdlem80 45546 caragenuncllem 45872 carageniuncllem1 45881 1fzopredsuc 46676 nnsum4primeseven 47112 nnsum4primesevenALTV 47113 lmod1 47532 iscnrm3rlem1 47931 |
Copyright terms: Public domain | W3C validator |