![]() |
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 4055 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1522 ∪ cun 3859 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-8 2082 ax-9 2090 ax-10 2111 ax-11 2125 ax-12 2140 ax-ext 2768 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1763 df-nf 1767 df-sb 2042 df-clab 2775 df-cleq 2787 df-clel 2862 df-nfc 2934 df-v 3438 df-un 3866 |
This theorem is referenced by: un12 4066 unundi 4069 undif1 4340 dfif5 4399 tpcoma 4595 qdass 4598 qdassr 4599 tpidm12 4600 symdifv 4909 unidif0 5154 difxp2 5902 resasplit 6419 fresaun 6420 fresaunres2 6421 df2o3 7971 sbthlem6 8482 fodomr 8518 domss2 8526 domunfican 8640 kmlem11 9435 hashfun 13646 prmreclem2 16082 setscom 16356 gsummptfzsplitl 18773 uniioombllem3 23869 lhop 24296 ex-un 27887 ex-pw 27892 indifundif 29966 cycpmrn 30414 bnj1415 31916 subfacp1lem1 32028 dftrpred4g 32676 lineunray 33211 bj-2upln1upl 33954 poimirlem3 34439 poimirlem4 34440 poimirlem5 34441 poimirlem16 34452 poimirlem17 34453 poimirlem19 34455 poimirlem20 34456 poimirlem22 34458 dfrcl2 39517 iunrelexp0 39545 trclfvdecomr 39571 corcltrcl 39582 cotrclrcl 39585 df3o2 39872 fourierdlem80 42027 caragenuncllem 42350 carageniuncllem1 42359 1fzopredsuc 43054 nnsum4primeseven 43461 nnsum4primesevenALTV 43462 lmod1 44041 |
Copyright terms: Public domain | W3C validator |