Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > unieqd | Unicode version |
Description: Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.) |
Ref | Expression |
---|---|
unieqd.1 |
Ref | Expression |
---|---|
unieqd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unieqd.1 | . 2 | |
2 | unieq 3792 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1342 cuni 3783 |
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 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-rex 2448 df-uni 3784 |
This theorem is referenced by: uniprg 3798 unisng 3800 unisn3 4417 onsucuni2 4535 opswapg 5084 elxp4 5085 elxp5 5086 iotaeq 5155 iotabi 5156 uniabio 5157 funfvdm 5543 funfvdm2 5544 fvun1 5546 fniunfv 5724 funiunfvdm 5725 1stvalg 6102 2ndvalg 6103 fo1st 6117 fo2nd 6118 f1stres 6119 f2ndres 6120 2nd1st 6140 cnvf1olem 6183 brtpos2 6210 dftpos4 6222 tpostpos 6223 recseq 6265 tfrexlem 6293 ixpsnf1o 6693 xpcomco 6783 xpassen 6787 xpdom2 6788 supeq1 6942 supeq2 6945 supeq3 6946 supeq123d 6947 en2other2 7143 dfinfre 8842 hashinfom 10680 hashennn 10682 fsumcnv 11364 fprodcnv 11552 isbasisg 12589 basis1 12592 baspartn 12595 tgval 12596 eltg 12599 ntrfval 12647 ntrval 12657 tgrest 12716 restuni2 12724 lmfval 12739 cnfval 12741 cnpfval 12742 txtopon 12809 txswaphmeolem 12867 peano4nninf 13727 |
Copyright terms: Public domain | W3C validator |