![]() |
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 3830 | . 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1363 ∪ cuni 3821 |
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 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2169 |
This theorem depends on definitions: df-bi 117 df-tru 1366 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-rex 2471 df-uni 3822 |
This theorem is referenced by: uniprg 3836 unisng 3838 unisn3 4457 onsucuni2 4575 opswapg 5127 elxp4 5128 elxp5 5129 iotaeq 5198 iotabi 5199 uniabio 5200 funfvdm 5592 funfvdm2 5593 fvun1 5595 fniunfv 5776 funiunfvdm 5777 1stvalg 6157 2ndvalg 6158 fo1st 6172 fo2nd 6173 f1stres 6174 f2ndres 6175 2nd1st 6195 cnvf1olem 6239 brtpos2 6266 dftpos4 6278 tpostpos 6279 recseq 6321 tfrexlem 6349 ixpsnf1o 6750 xpcomco 6840 xpassen 6844 xpdom2 6845 supeq1 6999 supeq2 7002 supeq3 7003 supeq123d 7004 en2other2 7209 dfinfre 8927 hashinfom 10772 hashennn 10774 fsumcnv 11459 fprodcnv 11647 tgval 12729 ptex 12731 lssuni 13552 lspuni0 13613 lss0v 13619 isbasisg 13840 basis1 13843 baspartn 13846 eltg 13848 ntrfval 13896 ntrval 13906 tgrest 13965 restuni2 13973 lmfval 13988 cnfval 13990 cnpfval 13991 txtopon 14058 txswaphmeolem 14116 peano4nninf 15052 |
Copyright terms: Public domain | W3C validator |