![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ineq2i | GIF version |
Description: Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.) |
Ref | Expression |
---|---|
ineq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
ineq2i | ⊢ (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ineq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | ineq2 3342 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵) |
Colors of variables: wff set class |
Syntax hints: = wceq 1363 ∩ cin 3140 |
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 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2169 |
This theorem depends on definitions: df-bi 117 df-tru 1366 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-v 2751 df-in 3147 |
This theorem is referenced by: in4 3363 inindir 3365 indif2 3391 difun1 3407 dfrab3ss 3425 dfif3 3559 intunsn 3894 rint0 3895 riin0 3970 res0 4923 resres 4931 resundi 4932 resindi 4934 inres 4936 resiun2 4939 resopab 4963 dfse2 5013 dminxp 5085 imainrect 5086 resdmres 5132 funimacnv 5304 unfiin 6938 sbthlemi5 6973 dmaddpi 7337 dmmulpi 7338 fsumiun 11498 ressval2 12539 ressval3d 12545 |
Copyright terms: Public domain | W3C validator |