![]() |
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 3988 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) | |
2 | uncom 3985 | . 2 ⊢ (𝐶 ∪ 𝐴) = (𝐴 ∪ 𝐶) | |
3 | uncom 3985 | . 2 ⊢ (𝐶 ∪ 𝐵) = (𝐵 ∪ 𝐶) | |
4 | 1, 2, 3 | 3eqtr4g 2887 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1658 ∪ cun 3797 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-ext 2804 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-v 3417 df-un 3804 |
This theorem is referenced by: uneq12 3990 uneq2i 3992 uneq2d 3995 uneqin 4109 disjssun 4260 uniprg 4673 unexb 7219 undifixp 8212 unxpdom 8437 ackbij1lem16 9373 fin23lem28 9478 ttukeylem6 9652 lcmfun 15732 ipodrsima 17519 mplsubglem 19796 mretopd 21268 iscldtop 21271 dfconn2 21594 nconnsubb 21598 comppfsc 21707 spanun 28960 locfinref 30454 isros 30777 unelros 30780 difelros 30781 rossros 30789 inelcarsg 30919 noextendseq 32360 rankung 32813 bj-funun 33680 paddval 35874 dochsatshp 37527 nacsfix 38120 eldioph4b 38220 eldioph4i 38221 fiuneneq 38619 isotone1 39187 fiiuncl 40052 |
Copyright terms: Public domain | W3C validator |