![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > unieqi | GIF version |
Description: Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993.) |
Ref | Expression |
---|---|
unieqi.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
unieqi | ⊢ ∪ 𝐴 = ∪ 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unieqi.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | unieq 3636 | . 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ ∪ 𝐴 = ∪ 𝐵 |
Colors of variables: wff set class |
Syntax hints: = 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: elunirab 3640 unisn 3643 uniop 4046 unisuc 4204 unisucg 4205 univ 4261 dfiun3g 4648 op1sta 4866 op2nda 4869 dfdm2 4919 iotajust 4933 dfiota2 4935 cbviota 4939 sb8iota 4941 dffv4g 5250 funfvdm2f 5314 riotauni 5553 1st0 5850 2nd0 5851 unielxp 5879 brtpos0 5949 recsfval 6012 uniqs 6280 xpassen 6476 sup00 6605 |
Copyright terms: Public domain | W3C validator |