![]() |
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 4156 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) | |
2 | uncom 4153 | . 2 ⊢ (𝐶 ∪ 𝐴) = (𝐴 ∪ 𝐶) | |
3 | uncom 4153 | . 2 ⊢ (𝐶 ∪ 𝐵) = (𝐵 ∪ 𝐶) | |
4 | 1, 2, 3 | 3eqtr4g 2791 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 ∪ cun 3945 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3464 df-un 3952 |
This theorem is referenced by: uneq12 4158 uneq2i 4160 uneq2d 4163 uneqin 4280 disjssun 4472 uniprgOLD 4934 unexb 7758 undifixp 8965 unfi 9212 unxpdom 9289 ackbij1lem16 10280 fin23lem28 10385 ttukeylem6 10559 lcmfun 16648 ipodrsima 18568 mplsubglem 22010 mretopd 23090 iscldtop 23093 dfconn2 23417 nconnsubb 23421 comppfsc 23530 noextendseq 27700 spanun 31481 locfinref 33658 isros 34003 unelros 34006 difelros 34007 rossros 34015 inelcarsg 34147 fineqvac 34935 rankung 35992 bj-funun 36961 paddval 39499 dochsatshp 41152 nacsfix 42387 eldioph4b 42486 eldioph4i 42487 fiuneneq 42875 isotone1 43733 fiiuncl 44684 |
Copyright terms: Public domain | W3C validator |