![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ineq1 | Structured version Visualization version GIF version |
Description: Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.) |
Ref | Expression |
---|---|
ineq1 | ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq2 2719 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
2 | 1 | anbi1d 741 | . . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))) |
3 | elin 3829 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶)) | |
4 | elin 3829 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) | |
5 | 2, 3, 4 | 3bitr4g 303 | . 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ 𝑥 ∈ (𝐵 ∩ 𝐶))) |
6 | 5 | eqrdv 2649 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1523 ∈ wcel 2030 ∩ cin 3606 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-v 3233 df-in 3614 |
This theorem is referenced by: ineq2 3841 ineq12 3842 ineq1i 3843 ineq1d 3846 unineq 3910 dfrab3ss 3938 intprg 4543 inex1g 4834 reseq1 5422 sspred 5726 isofrlem 6630 qsdisj 7867 fiint 8278 elfiun 8377 dffi3 8378 inf3lema 8559 dfac5lem5 8988 kmlem12 9021 kmlem14 9023 fin23lem24 9182 fin23lem26 9185 fin23lem23 9186 fin23lem22 9187 fin23lem27 9188 ingru 9675 uzin2 14128 incexclem 14612 elrestr 16136 firest 16140 inopn 20752 isbasisg 20799 basis1 20802 basis2 20803 tgval 20807 fctop 20856 cctop 20858 ntrfval 20876 elcls 20925 clsndisj 20927 elcls3 20935 neindisj2 20975 tgrest 21011 restco 21016 restsn 21022 restcld 21024 restcldi 21025 restopnb 21027 neitr 21032 restcls 21033 ordtbaslem 21040 ordtrest2lem 21055 hausnei2 21205 cnhaus 21206 regsep2 21228 dishaus 21234 ordthauslem 21235 cmpsublem 21250 cmpsub 21251 nconnsubb 21274 connsubclo 21275 1stcelcls 21312 islly 21319 cldllycmp 21346 lly1stc 21347 locfincmp 21377 elkgen 21387 ptclsg 21466 dfac14lem 21468 txrest 21482 pthaus 21489 txhaus 21498 xkohaus 21504 xkoptsub 21505 regr1lem 21590 isfbas 21680 fbasssin 21687 fbun 21691 isfil 21698 fbunfip 21720 fgval 21721 filconn 21734 uzrest 21748 isufil2 21759 hauspwpwf1 21838 fclsopni 21866 fclsnei 21870 fclsrest 21875 fcfnei 21886 fcfneii 21888 tsmsfbas 21978 ustincl 22058 ustdiag 22059 ustinvel 22060 ustexhalf 22061 ust0 22070 trust 22080 restutopopn 22089 lpbl 22355 methaus 22372 metrest 22376 restmetu 22422 qtopbaslem 22609 qdensere 22620 xrtgioo 22656 metnrmlem3 22711 icoopnst 22785 iocopnst 22786 ovolicc2lem2 23332 ovolicc2lem5 23335 mblsplit 23346 limcnlp 23687 ellimc3 23688 limcflf 23690 limciun 23703 ig1pval 23977 shincl 28368 shmodi 28377 omlsi 28391 pjoml 28423 chm0 28478 chincl 28486 chdmm1 28512 ledi 28527 cmbr 28571 cmbr3 28595 mdbr 29281 dmdmd 29287 dmdi 29289 dmdbr3 29292 dmdbr4 29293 mdslmd1lem4 29315 cvmd 29323 cvexch 29361 dmdbr6ati 29410 mddmdin0i 29418 difeq 29481 ofpreima2 29594 ordtrest2NEWlem 30096 inelsros 30369 diffiunisros 30370 measvuni 30405 measinb 30412 inelcarsg 30501 carsgclctunlem2 30509 totprob 30617 ballotlemgval 30713 cvmscbv 31366 cvmsdisj 31378 cvmsss2 31382 nepss 31725 brapply 32170 opnbnd 32445 isfne 32459 tailfb 32497 bj-restsn 33160 bj-restpw 33170 bj-rest0 33171 bj-restb 33172 ptrest 33538 poimirlem30 33569 mblfinlem2 33577 bndss 33715 lcvexchlem4 34642 fipjust 38187 ntrkbimka 38653 ntrk0kbimka 38654 clsk3nimkb 38655 isotone2 38664 ntrclskb 38684 ntrclsk3 38685 ntrclsk13 38686 elrestd 39605 islptre 40169 islpcn 40189 subsaliuncllem 40893 subsaliuncl 40894 nnfoctbdjlem 40990 caragensplit 41035 vonvolmbllem 41195 vonvolmbl 41196 incsmflem 41271 decsmflem 41295 smflimlem2 41301 smflimlem3 41302 smflim 41306 smfpimcclem 41334 uzlidlring 42254 rngcvalALTV 42286 rngcval 42287 ringcvalALTV 42332 ringcval 42333 |
Copyright terms: Public domain | W3C validator |