![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > uneq12 | Structured version Visualization version GIF version |
Description: Equality theorem for the union of two classes. (Contributed by NM, 29-Mar-1998.) |
Ref | Expression |
---|---|
uneq12 | ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uneq1 3983 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) | |
2 | uneq2 3984 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵 ∪ 𝐶) = (𝐵 ∪ 𝐷)) | |
3 | 1, 2 | sylan9eq 2834 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 = wceq 1601 ∪ cun 3790 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-v 3400 df-un 3797 |
This theorem is referenced by: uneq12i 3988 uneq12d 3991 un00 4237 opthprc 5415 dmpropg 5864 unixp 5924 fntpg 6196 fnun 6245 resasplit 6326 fvun 6530 rankprb 9013 pm54.43 9161 xpscg 16615 evlseu 19923 ptuncnv 22030 sshjval 28798 bj-2upleq 33580 poimirlem4 34048 poimirlem9 34053 diophun 38311 pwssplit4 38632 clsk1indlem3 39311 |
Copyright terms: Public domain | W3C validator |