Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > uneq2d | Unicode 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 3229 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1332 cun 3074 |
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 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-v 2691 df-un 3080 |
This theorem is referenced by: ifeq2 3483 tpeq3 3619 iununir 3904 unisucg 4344 relcoi1 5078 resasplitss 5310 fvun1 5495 fmptapd 5619 fvunsng 5622 fnsnsplitss 5627 tfr1onlemaccex 6253 tfrcllemaccex 6266 rdgeq1 6276 rdgivallem 6286 rdgisuc1 6289 rdgon 6291 rdg0 6292 oav2 6367 oasuc 6368 omv2 6369 omsuc 6376 fnsnsplitdc 6409 unsnfidcex 6816 undifdc 6820 fiintim 6825 ssfirab 6830 fnfi 6833 fidcenumlemr 6851 sbthlemi5 6857 sbthlemi6 6858 pm54.43 7063 fzsuc 9880 fseq1p1m1 9905 fseq1m1p1 9906 fzosplitsnm1 10017 fzosplitsn 10041 fzosplitprm1 10042 resunimafz0 10606 zfz1isolemsplit 10613 fsumm1 11217 ennnfonelemp1 11955 ennnfonelemhdmp1 11958 ennnfonelemkh 11961 ennnfonelemhf1o 11962 ennnfonelemnn0 11971 strsetsid 12031 setscom 12038 |
Copyright terms: Public domain | W3C validator |