![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > uneq12i | Unicode version |
Description: Equality inference for union of two classes. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
Ref | Expression |
---|---|
uneq1i.1 |
![]() ![]() ![]() ![]() |
uneq12i.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
uneq12i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uneq1i.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | uneq12i.2 |
. 2
![]() ![]() ![]() ![]() | |
3 | uneq12 3299 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | mp2an 426 |
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: indir 3399 difundir 3403 symdif1 3415 unrab 3421 rabun2 3429 dfif6 3551 dfif3 3562 unopab 4097 xpundi 4700 xpundir 4701 xpun 4705 dmun 4852 resundi 4938 resundir 4939 cnvun 5052 rnun 5055 imaundi 5059 imaundir 5060 dmtpop 5122 coundi 5148 coundir 5149 unidmrn 5179 dfdm2 5181 mptun 5366 fpr 5719 fvsnun2 5735 sbthlemi5 6990 djuunr 7095 djuun 7096 casedm 7115 djudm 7134 djuassen 7246 fz0to3un2pr 10153 fz0to4untppr 10154 fzo0to42pr 10250 |
Copyright terms: Public domain | W3C validator |