Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > uneq2 | Structured version Visualization version GIF version |
Description: Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
uneq2 | ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uneq1 3722 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) | |
2 | uncom 3719 | . 2 ⊢ (𝐶 ∪ 𝐴) = (𝐴 ∪ 𝐶) | |
3 | uncom 3719 | . 2 ⊢ (𝐶 ∪ 𝐵) = (𝐵 ∪ 𝐶) | |
4 | 1, 2, 3 | 3eqtr4g 2669 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = 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: uneq12 3724 uneq2i 3726 uneq2d 3729 uneqin 3837 disjssun 3988 uniprg 4386 unexb 6856 undifixp 7830 unxpdom 8052 ackbij1lem16 8940 fin23lem28 9045 ttukeylem6 9219 lcmfun 15196 ipodrsima 16988 mplsubglem 19255 mretopd 20706 iscldtop 20709 dfcon2 21032 nconsubb 21036 comppfsc 21145 spanun 27788 locfinref 29236 isros 29558 unelros 29561 difelros 29562 rossros 29570 inelcarsg 29700 nofulllem1 31101 rankung 31443 paddval 34102 dochsatshp 35758 nacsfix 36293 eldioph4b 36393 eldioph4i 36394 fiuneneq 36794 isotone1 37366 fiiuncl 38259 |
Copyright terms: Public domain | W3C validator |