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 4070 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1543 ∪ cun 3864 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3410 df-un 3871 |
This theorem is referenced by: un12 4081 unundi 4084 undif1 4390 dfif5 4455 tpcoma 4666 qdass 4669 qdassr 4670 tpidm12 4671 symdifv 4994 unidif0 5251 cnvimassrndm 6015 difxp2 6029 resasplit 6589 fresaun 6590 fresaunres2 6591 f1ofvswap 7116 df2o3 8217 sbthlem6 8761 fodomr 8797 domss2 8805 domunfican 8944 dftrpred4g 9340 kmlem11 9774 hashfun 14004 prmreclem2 16470 setscom 16733 gsummptfzsplitl 19318 uniioombllem3 24482 lhop 24913 ex-un 28507 ex-pw 28512 indifundif 30592 cycpmrn 31129 bnj1415 32731 subfacp1lem1 32854 sltlpss 33824 lineunray 34186 bj-2upln1upl 34951 poimirlem3 35517 poimirlem4 35518 poimirlem5 35519 poimirlem16 35530 poimirlem17 35531 poimirlem19 35533 poimirlem20 35534 poimirlem22 35536 metakunt24 39870 dfrcl2 40959 iunrelexp0 40987 trclfvdecomr 41013 corcltrcl 41024 cotrclrcl 41027 df3o2 41311 fourierdlem80 43402 caragenuncllem 43725 carageniuncllem1 43734 1fzopredsuc 44489 nnsum4primeseven 44925 nnsum4primesevenALTV 44926 lmod1 45506 iscnrm3rlem1 45907 |
Copyright terms: Public domain | W3C validator |