![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ineq2i | 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 |
---|---|
ineq2i | ⊢ (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ineq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | ineq2 4206 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 ∩ cin 3945 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-in 3953 |
This theorem is referenced by: in4 4226 inindir 4228 indif2 4271 difun1 4290 dfrab3ss 4314 undif1 4479 difdifdir 4495 dfif3 4546 dfif5 4548 disjpr2 4721 disjprsn 4722 disjtp2 4724 intunsn 4996 rint0 4997 riin0 5089 csbres 5991 res0 5992 resres 6001 resundi 6002 resindi 6004 inres 6006 resiun2 6009 resopab 6042 dffr3 6108 dfse2 6109 dminxp 6190 imainrect 6191 cnvrescnv 6205 resdmres 6242 resdifdi 6246 dfpo2 6306 snres0 6308 dfpred2 6321 predidm 6338 funimacnv 6639 fresaun 6772 fresaunres2 6773 wfrlem13OLD 8350 tfrlem10 8416 sbthlem5 9124 infssuni 9383 dfsup2 9483 en3lplem2 9652 wemapwe 9736 epfrs 9770 r0weon 10051 infxpenlem 10052 kmlem11 10199 ackbij1lem1 10259 ackbij1lem2 10260 axdc3lem4 10492 canthwelem 10689 dmaddpi 10929 dmmulpi 10930 ssxr 11329 dmhashres 14353 fz1isolem 14475 f1oun2prg 14921 fsumiun 15820 sadeq 16467 bitsres 16468 smuval2 16477 smumul 16488 ressinbas 17254 lubdm 18371 glbdm 18384 sylow2a 19612 lsmmod2 19669 lsmdisj2r 19678 ablfac1eu 20068 pjdm 21697 ressmplbas2 22026 opsrtoslem1 22060 rintopn 22894 ordtrest2 23191 cmpsublem 23386 kgentopon 23525 hausdiag 23632 uzrest 23884 ufprim 23896 trust 24217 metnrmlem3 24860 clsocv 25261 ismbl 25538 unmbl 25549 volinun 25558 voliunlem1 25562 ovolioo 25580 itg2cnlem2 25775 ellimc2 25889 limcflf 25893 lhop1lem 26029 lgsquadlem3 27403 rplogsum 27548 noextend 27688 noextendseq 27689 noetasuplem2 27756 noetainflem2 27760 madeval2 27869 umgrislfupgrlem 29050 spthispth 29655 0pth 30050 1pthdlem2 30061 frgrncvvdeqlem3 30226 ex-in 30350 chdmj3i 31408 chdmj4i 31409 chjassi 31411 pjoml2i 31510 pjoml3i 31511 cmcmlem 31516 cmcm2i 31518 cmbr3i 31525 fh3i 31548 fh4i 31549 osumcor2i 31569 mayetes3i 31654 mdslmd3i 32257 mdexchi 32260 atabsi 32326 dmdbr5ati 32347 inin 32433 uniin2 32464 of0r 32587 dfprm3 33405 ordtrest2NEW 33694 hasheuni 33874 carsgclctunlem1 34107 eulerpartgbij 34162 fiblem 34188 cvmscld 35053 sate0 35195 msrid 35325 elrn3 35532 bj-inrab3 36583 poimirlem15 37284 mblfinlem2 37307 ftc1anclem6 37347 xrnres2 38049 redundss3 38274 refrelsredund4 38278 pol0N 39556 mapfzcons2 42313 diophrw 42353 conrel2d 43268 iunrelexp0 43306 hashnzfz 43931 disjinfi 44736 fourierdlem80 45744 sge0resplit 45964 sge0split 45967 caragenuncllem 46070 iscnrm3rlem1 48211 |
Copyright terms: Public domain | W3C validator |