![]() |
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 3911 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) | |
2 | uneq2 3912 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵 ∪ 𝐶) = (𝐵 ∪ 𝐷)) | |
3 | 1, 2 | sylan9eq 2825 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 = wceq 1631 ∪ cun 3721 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-v 3353 df-un 3728 |
This theorem is referenced by: uneq12i 3916 uneq12d 3919 un00 4155 opthprc 5307 dmpropg 5750 unixp 5812 fntpg 6089 fnun 6137 resasplit 6214 fvun 6410 rankprb 8878 pm54.43 9026 xpscg 16426 evlseu 19731 ptuncnv 21831 sshjval 28549 bj-2upleq 33331 poimirlem4 33746 poimirlem9 33751 diophun 37863 pwssplit4 38185 clsk1indlem3 38867 |
Copyright terms: Public domain | W3C validator |