![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > unieqd | GIF version |
Description: Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.) |
Ref | Expression |
---|---|
unieqd.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
unieqd | ⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unieqd.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | unieq 3636 | . 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1285 ∪ cuni 3627 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 |
This theorem depends on definitions: df-bi 115 df-tru 1288 df-nf 1391 df-sb 1688 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-rex 2359 df-uni 3628 |
This theorem is referenced by: uniprg 3642 unisng 3644 unisn3 4233 onsucuni2 4342 opswapg 4870 elxp4 4871 elxp5 4872 iotaeq 4941 iotabi 4942 uniabio 4943 funfvdm 5311 funfvdm2 5312 fvun1 5314 fniunfv 5480 funiunfvdm 5481 1stvalg 5847 2ndvalg 5848 fo1st 5862 fo2nd 5863 f1stres 5864 f2ndres 5865 2nd1st 5884 cnvf1olem 5923 brtpos2 5947 dftpos4 5959 tpostpos 5960 recseq 6002 tfrexlem 6030 xpcomco 6471 xpassen 6475 xpdom2 6476 supeq1 6587 supeq2 6590 supeq3 6591 supeq123d 6592 en2other2 6724 dfinfre 8310 hashinfom 10020 hashennn 10022 |
Copyright terms: Public domain | W3C validator |