| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ineq1i | Structured version Visualization version GIF version | ||
| Description: Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.) |
| Ref | Expression |
|---|---|
| ineq1i.1 | ⊢ 𝐴 = 𝐵 |
| Ref | Expression |
|---|---|
| ineq1i | ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ineq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
| 2 | ineq1 4213 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∩ cin 3950 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-in 3958 |
| This theorem is referenced by: in12 4229 inindi 4235 dfrab3 4319 dfif5 4542 disjpr2 4713 disjtpsn 4715 disjtp2 4716 resres 6010 imainrect 6201 predidm 6347 fresaun 6779 fresaunres2 6780 ssenen 9191 hartogslem1 9582 prinfzo0 13738 leiso 14498 f1oun2prg 14956 smumul 16530 setsfun 17208 setsfun0 17209 firest 17477 lsmdisj2r 19703 frgpuplem 19790 ltbwe 22062 tgrest 23167 fiuncmp 23412 ptclsg 23623 metnrmlem3 24883 mbfid 25670 ppi1 27207 cht1 27208 ppiub 27248 lrrecse 27975 lrrecpred 27977 chdmj2i 31501 chjassi 31505 pjoml2i 31604 pjoml4i 31606 cmcmlem 31610 mayetes3i 31748 cvmdi 32343 atomli 32401 atabsi 32420 uniin1 32564 disjuniel 32610 imadifxp 32614 gtiso 32710 preiman0 32719 nn0disj01 32820 prsss 33915 ordtrest2NEW 33922 esumnul 34049 measinblem 34221 eulerpartlemt 34373 ballotlem2 34491 ballotlemfp1 34494 ballotlemfval0 34498 chtvalz 34644 fmla0disjsuc 35403 mthmpps 35587 dffv5 35925 bj-sscon 37030 bj-discrmoore 37112 mblfinlem2 37665 ismblfin 37668 mbfposadd 37674 itg2addnclem2 37679 asindmre 37710 abeqin 38253 xrnres 38403 redundeq1 38630 refrelsredund4 38633 diophrw 42770 dnwech 43060 lmhmlnmsplit 43099 rp-fakeuninass 43529 iunrelexp0 43715 nznngen 44335 uzinico2 45575 limsup0 45709 limsupvaluz 45723 sge0sn 46394 31prm 47584 |
| Copyright terms: Public domain | W3C validator |