![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > uneq2d | GIF version |
Description: Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.) |
Ref | Expression |
---|---|
uneq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
uneq2d | ⊢ (𝜑 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uneq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | uneq2 3130 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1285 ∪ cun 2980 |
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-v 2612 df-un 2986 |
This theorem is referenced by: ifeq2 3372 tpeq3 3498 iununir 3779 unisucg 4197 relcoi1 4899 resasplitss 5120 fvun1 5291 fmptapd 5406 fvunsng 5409 tfr1onlemaccex 6017 tfrcllemaccex 6030 rdgeq1 6040 rdgivallem 6050 rdgisuc1 6053 rdgon 6055 rdg0 6056 oav2 6127 oasuc 6128 omv2 6129 omsuc 6136 unsnfidcex 6464 undifdc 6468 ssfirab 6475 fnfi 6478 pm54.43 6570 fzsuc 9214 fseq1p1m1 9239 fseq1m1p1 9240 fzosplitsnm1 9347 fzosplitsn 9371 fzosplitprm1 9372 |
Copyright terms: Public domain | W3C validator |