![]() |
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 3958 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1631 ∩ cin 3722 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-v 3353 df-in 3730 |
This theorem is referenced by: in12 3973 inindi 3979 dfrab3 4050 dfif5 4241 disjpr2 4385 disjtpsn 4387 disjtp2 4388 resres 5548 imainrect 5714 predidm 5843 fresaun 6213 fresaunres2 6214 ssenen 8288 hartogslem1 8601 prinfzo0 12708 leiso 13438 f1oun2prg 13864 smumul 15416 setsfun 16093 setsfun0 16094 firest 16294 lsmdisj2r 18298 frgpuplem 18385 ltbwe 19680 tgrest 21177 fiuncmp 21421 ptclsg 21632 metnrmlem3 22877 mbfid 23616 ppi1 25104 cht1 25105 ppiub 25143 chdmj2i 28674 chjassi 28678 pjoml2i 28777 pjoml4i 28779 cmcmlem 28783 mayetes3i 28921 cvmdi 29516 atomli 29574 atabsi 29593 uniin1 29698 disjuniel 29741 imadifxp 29745 gtiso 29811 prsss 30295 ordtrest2NEW 30302 esumnul 30443 measinblem 30616 eulerpartlemt 30766 ballotlem2 30883 ballotlemfp1 30886 ballotlemfval0 30890 chtvalz 31040 mthmpps 31810 dffv5 32361 bj-sscon 33338 bj-discrmoore 33391 mblfinlem2 33773 ismblfin 33776 mbfposadd 33782 itg2addnclem2 33787 asindmre 33820 abeqin 34353 xrnres 34495 diophrw 37841 dnwech 38137 lmhmlnmsplit 38176 rp-fakeuninass 38381 iunrelexp0 38513 nznngen 39034 uzinico2 40300 limsup0 40437 limsupvaluz 40451 sge0sn 41106 31prm 42033 |
Copyright terms: Public domain | W3C validator |