| 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 4214 | . 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-tru 1543 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: in4 4234 inindir 4236 indif2 4281 difun1 4299 dfrab3ss 4323 undif1 4476 difdifdir 4492 dfif3 4540 dfif5 4542 disjpr2 4713 disjprsn 4714 disjtp2 4716 intunsn 4987 rint0 4988 riin0 5082 csbres 6000 res0 6001 resres 6010 resundi 6011 resindi 6013 inres 6015 resiun2 6018 resopab 6052 dffr3 6117 dfse2 6118 dminxp 6200 imainrect 6201 cnvrescnv 6215 resdmres 6252 resdifdi 6256 dfpo2 6316 snres0 6318 dfpred2 6331 predidm 6347 funimacnv 6647 fresaun 6779 fresaunres2 6780 wfrlem13OLD 8361 tfrlem10 8427 sbthlem5 9127 infssuni 9386 dfsup2 9484 en3lplem2 9653 wemapwe 9737 epfrs 9771 r0weon 10052 infxpenlem 10053 kmlem11 10201 ackbij1lem1 10259 ackbij1lem2 10260 axdc3lem4 10493 canthwelem 10690 dmaddpi 10930 dmmulpi 10931 ssxr 11330 dmhashres 14380 fz1isolem 14500 f1oun2prg 14956 fsumiun 15857 sadeq 16509 bitsres 16510 smuval2 16519 smumul 16530 ressinbas 17291 lubdm 18396 glbdm 18409 sylow2a 19637 lsmmod2 19694 lsmdisj2r 19703 ablfac1eu 20093 pjdm 21727 ressmplbas2 22045 opsrtoslem1 22079 rintopn 22915 ordtrest2 23212 cmpsublem 23407 kgentopon 23546 hausdiag 23653 uzrest 23905 ufprim 23917 trust 24238 metnrmlem3 24883 clsocv 25284 ismbl 25561 unmbl 25572 volinun 25581 voliunlem1 25585 ovolioo 25603 itg2cnlem2 25797 ellimc2 25912 limcflf 25916 lhop1lem 26052 lgsquadlem3 27426 rplogsum 27571 noextend 27711 noextendseq 27712 noetasuplem2 27779 noetainflem2 27783 madeval2 27892 umgrislfupgrlem 29139 spthispth 29744 cyclnumvtx 29820 0pth 30144 1pthdlem2 30155 frgrncvvdeqlem3 30320 ex-in 30444 chdmj3i 31502 chdmj4i 31503 chjassi 31505 pjoml2i 31604 pjoml3i 31605 cmcmlem 31610 cmcm2i 31612 cmbr3i 31619 fh3i 31642 fh4i 31643 osumcor2i 31663 mayetes3i 31748 mdslmd3i 32351 mdexchi 32354 atabsi 32420 dmdbr5ati 32441 inin 32535 uniin2 32565 of0r 32688 dfprm3 33581 ordtrest2NEW 33922 hasheuni 34086 carsgclctunlem1 34319 eulerpartgbij 34374 fiblem 34400 cvmscld 35278 sate0 35420 msrid 35550 elrn3 35762 bj-inrab3 36930 poimirlem15 37642 mblfinlem2 37665 ftc1anclem6 37705 xrnres2 38404 redundss3 38629 refrelsredund4 38633 pol0N 39911 readvrec2 42391 mapfzcons2 42730 diophrw 42770 conrel2d 43677 iunrelexp0 43715 hashnzfz 44339 wfaxpow 45014 disjinfi 45197 fourierdlem80 46201 sge0resplit 46421 sge0split 46424 caragenuncllem 46527 iscnrm3rlem1 48837 |
| Copyright terms: Public domain | W3C validator |