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 3589 | . 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1243 ∪ cuni 3580 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-tru 1246 df-nf 1350 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-nfc 2167 df-rex 2312 df-uni 3581 |
This theorem is referenced by: uniprg 3595 unisng 3597 unisn3 4180 onsucuni2 4288 opswapg 4807 elxp4 4808 elxp5 4809 iotaeq 4875 iotabi 4876 uniabio 4877 funfvdm 5236 funfvdm2 5237 fvun1 5239 fniunfv 5401 funiunfvdm 5402 1stvalg 5769 2ndvalg 5770 fo1st 5784 fo2nd 5785 f1stres 5786 f2ndres 5787 2nd1st 5806 cnvf1olem 5845 brtpos2 5866 dftpos4 5878 tpostpos 5879 recseq 5921 tfrexlem 5948 xpcomco 6300 xpassen 6304 xpdom2 6305 |
Copyright terms: Public domain | W3C validator |