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 3745 | . 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1331 ∪ cuni 3736 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-rex 2422 df-uni 3737 |
This theorem is referenced by: uniprg 3751 unisng 3753 unisn3 4366 onsucuni2 4479 opswapg 5025 elxp4 5026 elxp5 5027 iotaeq 5096 iotabi 5097 uniabio 5098 funfvdm 5484 funfvdm2 5485 fvun1 5487 fniunfv 5663 funiunfvdm 5664 1stvalg 6040 2ndvalg 6041 fo1st 6055 fo2nd 6056 f1stres 6057 f2ndres 6058 2nd1st 6078 cnvf1olem 6121 brtpos2 6148 dftpos4 6160 tpostpos 6161 recseq 6203 tfrexlem 6231 ixpsnf1o 6630 xpcomco 6720 xpassen 6724 xpdom2 6725 supeq1 6873 supeq2 6876 supeq3 6877 supeq123d 6878 en2other2 7052 dfinfre 8714 hashinfom 10524 hashennn 10526 fsumcnv 11206 isbasisg 12211 basis1 12214 baspartn 12217 tgval 12218 eltg 12221 ntrfval 12269 ntrval 12279 tgrest 12338 restuni2 12346 lmfval 12361 cnfval 12363 cnpfval 12364 txtopon 12431 txswaphmeolem 12489 peano4nninf 13200 |
Copyright terms: Public domain | W3C validator |