![]() |
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 3298 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
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 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-v 2754 df-un 3148 |
This theorem is referenced by: ifeq2 3553 tpeq3 3695 iununir 3985 unisucg 4429 relcoi1 5175 resasplitss 5410 fvun1 5598 fmptapd 5723 fvunsng 5726 fnsnsplitss 5731 tfr1onlemaccex 6367 tfrcllemaccex 6380 rdgeq1 6390 rdgivallem 6400 rdgisuc1 6403 rdgon 6405 rdg0 6406 oav2 6482 oasuc 6483 omv2 6484 omsuc 6491 fnsnsplitdc 6524 unsnfidcex 6937 undifdc 6941 fiintim 6946 ssfirab 6951 fnfi 6954 fidcenumlemr 6972 sbthlemi5 6978 sbthlemi6 6979 pm54.43 7207 fzsuc 10087 fseq1p1m1 10112 fseq1m1p1 10113 fzosplitsnm1 10227 fzosplitsn 10251 fzosplitprm1 10252 resunimafz0 10829 zfz1isolemsplit 10836 fsumm1 11442 fprodm1 11624 ennnfonelemp1 12425 ennnfonelemhdmp1 12428 ennnfonelemkh 12431 ennnfonelemhf1o 12432 ennnfonelemnn0 12441 strsetsid 12513 setscom 12520 lspun0 13702 bj-charfundcALT 14945 |
Copyright terms: Public domain | W3C validator |