![]() |
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 4071 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1507 ∩ cin 3829 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2751 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2760 df-cleq 2772 df-clel 2847 df-nfc 2919 df-rab 3098 df-v 3418 df-in 3837 |
This theorem is referenced by: in4 4090 inindir 4092 indif2 4135 difun1 4152 dfrab3ss 4169 undif1 4307 difdifdir 4320 dfif3 4364 dfif5 4366 disjpr2 4523 disjprsn 4524 disjtp2 4526 intunsn 4788 rint0 4789 riin0 4870 csbres 5698 res0 5699 resres 5711 resundi 5712 resindi 5714 inres 5716 resiun2 5719 resopab 5747 dffr3 5802 dfse2 5803 dminxp 5877 imainrect 5878 resdmres 5928 dfpred2 5995 predidm 6008 funimacnv 6268 fresaun 6378 fresaunres2 6379 wfrlem13 7771 tfrlem10 7827 sbthlem5 8427 infssuni 8610 dfsup2 8703 en3lplem2 8870 wemapwe 8954 epfrs 8967 r0weon 9232 infxpenlem 9233 kmlem11 9380 ackbij1lem1 9440 ackbij1lem2 9441 axdc3lem4 9673 canthwelem 9870 dmaddpi 10110 dmmulpi 10111 ssxr 10510 dmhashres 13516 fz1isolem 13632 f1oun2prg 14141 fsumiun 15036 sadeq 15681 bitsres 15682 smuval2 15691 smumul 15702 ressinbas 16416 lubdm 17447 glbdm 17460 sylow2a 18505 lsmmod2 18560 lsmdisj2r 18569 ablfac1eu 18945 ressmplbas2 19949 opsrtoslem1 19977 pjdm 20553 rintopn 21221 ordtrest2 21516 cmpsublem 21711 kgentopon 21850 hausdiag 21957 uzrest 22209 ufprim 22221 trust 22541 metnrmlem3 23172 clsocv 23556 ismbl 23830 unmbl 23841 volinun 23850 voliunlem1 23854 ovolioo 23872 itg2cnlem2 24066 ellimc2 24178 limcflf 24182 lhop1lem 24313 lgsquadlem3 25660 rplogsum 25805 umgrislfupgrlem 26610 spthispth 27215 0pth 27654 1pthdlem2 27665 frgrncvvdeqlem3 27835 ex-in 27982 chdmj3i 29041 chdmj4i 29042 chjassi 29044 pjoml2i 29143 pjoml3i 29144 cmcmlem 29149 cmcm2i 29151 cmbr3i 29158 fh3i 29181 fh4i 29182 osumcor2i 29202 mayetes3i 29287 mdslmd3i 29890 mdexchi 29893 atabsi 29959 dmdbr5ati 29980 inin 30053 uniin2 30072 ordtrest2NEW 30807 hasheuni 30985 carsgclctunlem1 31217 eulerpartgbij 31272 fiblem 31299 cvmscld 32102 msrid 32309 dfpo2 32508 elrn3 32515 noextend 32691 noextendseq 32692 madeval2 32808 bj-inrab3 33739 poimirlem15 34345 mblfinlem2 34368 ftc1anclem6 34410 xrnres2 35093 redundss3 35305 refrelsredund4 35309 pol0N 36487 mapfzcons2 38708 diophrw 38748 conrel2d 39369 iunrelexp0 39407 hashnzfz 40065 disjinfi 40876 fourierdlem80 41900 sge0resplit 42117 sge0split 42120 caragenuncllem 42223 |
Copyright terms: Public domain | W3C validator |