![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > uneq12d | GIF version |
Description: Equality deduction for union of two classes. (Contributed by NM, 29-Sep-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Ref | Expression |
---|---|
uneq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
uneq12d.2 | ⊢ (𝜑 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
uneq12d | ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uneq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | uneq12d.2 | . 2 ⊢ (𝜑 → 𝐶 = 𝐷) | |
3 | uneq12 3308 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)) | |
4 | 1, 2, 3 | syl2anc 411 | 1 ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1364 ∪ cun 3151 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2175 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-v 2762 df-un 3157 |
This theorem is referenced by: disjpr2 3682 diftpsn3 3759 iunxprg 3993 undifexmid 4222 exmidundif 4235 exmidundifim 4236 exmid1stab 4237 suceq 4433 rnpropg 5145 fntpg 5310 foun 5519 fnimapr 5617 fprg 5741 fsnunfv 5759 fsnunres 5760 tfrlemi1 6385 tfr1onlemaccex 6401 tfrcllemaccex 6414 ereq1 6594 undifdc 6980 unfiin 6982 djueq12 7098 fztp 10144 fzsuc2 10145 fseq1p1m1 10160 ennnfonelemg 12560 ennnfonelemp1 12563 ennnfonelem1 12564 ennnfonelemnn0 12579 setsvalg 12648 setsfun0 12654 setsresg 12656 setsslid 12669 prdsex 12880 psrval 14152 |
Copyright terms: Public domain | W3C validator |