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 3770 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 ∩ cin 3539 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-in 3547 |
This theorem is referenced by: in4 3791 inindir 3793 indif2 3829 difun1 3846 dfrab3ss 3864 undif1 3995 difdifdir 4008 dfif3 4050 dfif5 4052 disjpr2 4194 disjprsn 4196 intunsn 4451 rint0 4452 riin0 4530 csbres 5320 res0 5321 resres 5329 resundi 5330 resindi 5332 inres 5334 resiun2 5338 resopab 5366 dffr3 5417 dfse2 5418 dminxp 5493 imainrect 5494 resdmres 5543 dfpred2 5606 predidm 5619 funimacnv 5884 fresaun 5988 fresaunres2 5989 wfrlem13 7314 tfrlem10 7370 sbthlem5 7959 infssuni 8140 dfsup2 8233 en3lplem2 8395 wemapwe 8477 epfrs 8490 r0weon 8718 infxpenlem 8719 kmlem11 8865 ackbij1lem1 8925 ackbij1lem2 8926 axdc3lem4 9158 canthwelem 9351 dmaddpi 9591 dmmulpi 9592 ssxr 9986 dmhashres 12991 fz1isolem 13102 f1oun2prg 13512 fsumiun 14394 sadeq 15032 bitsres 15033 smuval2 15042 smumul 15053 ressinbas 15763 lubdm 16802 glbdm 16815 sylow2a 17857 lsmmod2 17912 lsmdisj2r 17921 ablfac1eu 18295 ressmplbas2 19276 opsrtoslem1 19305 pjdm 19870 rintopn 20539 ordtrest2 20818 cmpsublem 21012 kgentopon 21151 hausdiag 21258 uzrest 21511 ufprim 21523 trust 21843 metnrmlem3 22472 clsocv 22857 ismbl 23101 unmbl 23112 volinun 23121 voliunlem1 23125 ovolioo 23143 itg2cnlem2 23335 ellimc2 23447 limcflf 23451 lhop1lem 23580 lgsquadlem3 24907 rplogsum 25016 umgrislfupgrlem 25788 0pth 26100 1pthonlem2 26120 frgrancvvdeqlem4 26560 ex-in 26674 chdmj3i 27726 chdmj4i 27727 chjassi 27729 pjoml2i 27828 pjoml3i 27829 cmcmlem 27834 cmcm2i 27836 cmbr3i 27843 fh3i 27866 fh4i 27867 osumcor2i 27887 mayetes3i 27972 mdslmd3i 28575 mdexchi 28578 atabsi 28644 dmdbr5ati 28665 inin 28737 uniin2 28751 ordtrest2NEW 29297 hasheuni 29474 carsgclctunlem1 29706 eulerpartgbij 29761 fiblem 29787 cvmscld 30509 msrid 30696 dfpo2 30898 elrn3 30906 bj-inrab3 32117 poimirlem15 32594 mblfinlem2 32617 ftc1anclem6 32660 pol0N 34213 mapfzcons2 36300 diophrw 36340 conrel2d 36975 iunrelexp0 37013 hashnzfz 37541 disjinfi 38375 fourierdlem80 39079 sge0resplit 39299 sge0split 39302 caragenuncllem 39402 sPthisPth 40932 0pth-av 41293 1pthdlem2 41303 frgrncvvdeqlem4 41472 |
Copyright terms: Public domain | W3C validator |