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 3722 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 ∪ cun 3538 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-un 3545 |
This theorem is referenced by: un12 3733 unundi 3736 undif1 3995 dfif5 4052 tpcoma 4229 qdass 4232 qdassr 4233 tpidm12 4234 symdifv 4534 unidif0 4764 difxp2 5479 resasplit 5987 fresaun 5988 fresaunres2 5989 df2o3 7460 sbthlem6 7960 fodomr 7996 domss2 8004 domunfican 8118 kmlem11 8865 hashfun 13084 prmreclem2 15459 setscom 15731 gsummptfzsplitl 18156 uniioombllem3 23159 lhop 23583 usgrafilem1 25940 constr3pthlem1 26183 ex-un 26673 ex-pw 26678 indifundif 28740 bnj1415 30360 subfacp1lem1 30415 dftrpred4g 30978 lineunray 31424 bj-2upln1upl 32205 poimirlem3 32582 poimirlem4 32583 poimirlem5 32584 poimirlem16 32595 poimirlem17 32596 poimirlem19 32598 poimirlem20 32599 poimirlem22 32601 dfrcl2 36985 iunrelexp0 37013 trclfvdecomr 37039 corcltrcl 37050 cotrclrcl 37053 df3o2 37342 fourierdlem80 39079 caragenuncllem 39402 carageniuncllem1 39411 1fzopredsuc 39947 nnsum4primeseven 40216 nnsum4primesevenALTV 40217 lmod1 42075 |
Copyright terms: Public domain | W3C validator |