![]() |
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 4166 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 ∩ cin 3909 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-rab 3408 df-in 3917 |
This theorem is referenced by: in4 4185 inindir 4187 indif2 4230 difun1 4249 dfrab3ss 4272 undif1 4435 difdifdir 4449 dfif3 4500 dfif5 4502 disjpr2 4674 disjprsn 4675 disjtp2 4677 intunsn 4950 rint0 4951 riin0 5042 csbres 5940 res0 5941 resres 5950 resundi 5951 resindi 5953 inres 5955 resiun2 5958 resopab 5988 dffr3 6051 dfse2 6052 dminxp 6132 imainrect 6133 cnvrescnv 6147 resdmres 6184 resdifdi 6188 dfpo2 6248 snres0 6250 dfpred2 6263 predidm 6280 funimacnv 6582 fresaun 6713 fresaunres2 6714 wfrlem13OLD 8266 tfrlem10 8332 sbthlem5 9030 infssuni 9286 dfsup2 9379 en3lplem2 9548 wemapwe 9632 epfrs 9666 r0weon 9947 infxpenlem 9948 kmlem11 10095 ackbij1lem1 10155 ackbij1lem2 10156 axdc3lem4 10388 canthwelem 10585 dmaddpi 10825 dmmulpi 10826 ssxr 11223 dmhashres 14240 fz1isolem 14359 f1oun2prg 14805 fsumiun 15705 sadeq 16351 bitsres 16352 smuval2 16361 smumul 16372 ressinbas 17125 lubdm 18239 glbdm 18252 sylow2a 19399 lsmmod2 19456 lsmdisj2r 19465 ablfac1eu 19850 pjdm 21111 ressmplbas2 21426 opsrtoslem1 21460 rintopn 22256 ordtrest2 22553 cmpsublem 22748 kgentopon 22887 hausdiag 22994 uzrest 23246 ufprim 23258 trust 23579 metnrmlem3 24222 clsocv 24612 ismbl 24888 unmbl 24899 volinun 24908 voliunlem1 24912 ovolioo 24930 itg2cnlem2 25125 ellimc2 25239 limcflf 25243 lhop1lem 25375 lgsquadlem3 26728 rplogsum 26873 noextend 27012 noextendseq 27013 noetasuplem2 27080 noetainflem2 27084 madeval2 27181 umgrislfupgrlem 28020 spthispth 28621 0pth 29016 1pthdlem2 29027 frgrncvvdeqlem3 29192 ex-in 29316 chdmj3i 30372 chdmj4i 30373 chjassi 30375 pjoml2i 30474 pjoml3i 30475 cmcmlem 30480 cmcm2i 30482 cmbr3i 30489 fh3i 30512 fh4i 30513 osumcor2i 30533 mayetes3i 30618 mdslmd3i 31221 mdexchi 31224 atabsi 31290 dmdbr5ati 31311 inin 31389 uniin2 31418 ordtrest2NEW 32444 hasheuni 32624 carsgclctunlem1 32857 eulerpartgbij 32912 fiblem 32938 cvmscld 33807 sate0 33949 msrid 34079 elrn3 34275 bj-inrab3 35389 poimirlem15 36083 mblfinlem2 36106 ftc1anclem6 36146 xrnres2 36855 redundss3 37080 refrelsredund4 37084 pol0N 38362 mapfzcons2 41019 diophrw 41059 conrel2d 41917 iunrelexp0 41955 hashnzfz 42581 disjinfi 43387 fourierdlem80 44398 sge0resplit 44618 sge0split 44621 caragenuncllem 44724 iscnrm3rlem1 46944 |
Copyright terms: Public domain | W3C validator |