![]() |
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 3895 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) | |
2 | uncom 3892 | . 2 ⊢ (𝐶 ∪ 𝐴) = (𝐴 ∪ 𝐶) | |
3 | uncom 3892 | . 2 ⊢ (𝐶 ∪ 𝐵) = (𝐵 ∪ 𝐶) | |
4 | 1, 2, 3 | 3eqtr4g 2811 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1624 ∪ cun 3705 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-v 3334 df-un 3712 |
This theorem is referenced by: uneq12 3897 uneq2i 3899 uneq2d 3902 uneqin 4013 disjssun 4172 uniprg 4594 unexb 7115 undifixp 8102 unxpdom 8324 ackbij1lem16 9241 fin23lem28 9346 ttukeylem6 9520 lcmfun 15552 ipodrsima 17358 mplsubglem 19628 mretopd 21090 iscldtop 21093 dfconn2 21416 nconnsubb 21420 comppfsc 21529 spanun 28705 locfinref 30209 isros 30532 unelros 30535 difelros 30536 rossros 30544 inelcarsg 30674 noextendseq 32118 rankung 32571 paddval 35579 dochsatshp 37234 nacsfix 37769 eldioph4b 37869 eldioph4i 37870 fiuneneq 38269 isotone1 38840 fiiuncl 39725 |
Copyright terms: Public domain | W3C validator |