![]() |
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 3163 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-v 2635 df-un 3017 |
This theorem is referenced by: ifeq2 3417 tpeq3 3550 iununir 3834 unisucg 4265 relcoi1 4996 resasplitss 5225 fvun1 5405 fmptapd 5527 fvunsng 5530 fnsnsplitss 5535 tfr1onlemaccex 6151 tfrcllemaccex 6164 rdgeq1 6174 rdgivallem 6184 rdgisuc1 6187 rdgon 6189 rdg0 6190 oav2 6264 oasuc 6265 omv2 6266 omsuc 6273 fnsnsplitdc 6304 unsnfidcex 6710 undifdc 6714 fiintim 6719 ssfirab 6723 fnfi 6726 fidcenumlemr 6744 sbthlemi5 6750 sbthlemi6 6751 pm54.43 6915 fzsuc 9632 fseq1p1m1 9657 fseq1m1p1 9658 fzosplitsnm1 9769 fzosplitsn 9793 fzosplitprm1 9794 resunimafz0 10367 zfz1isolemsplit 10374 fsumm1 10975 strsetsid 11692 setscom 11699 |
Copyright terms: Public domain | W3C validator |