![]() |
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 2677 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
2 | 1 | anbi1d 737 | . . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))) |
3 | elin 3758 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶)) | |
4 | elin 3758 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) | |
5 | 2, 3, 4 | 3bitr4g 302 | . 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ 𝑥 ∈ (𝐵 ∩ 𝐶))) |
6 | 5 | eqrdv 2608 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ∩ 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: ineq2 3770 ineq12 3771 ineq1i 3772 ineq1d 3775 unineq 3836 dfrab3ss 3864 intprg 4446 inex1g 4729 reseq1 5311 sspred 5605 isofrlem 6490 qsdisj 7711 fiint 8122 elfiun 8219 dffi3 8220 inf3lema 8404 dfac5lem5 8833 kmlem12 8866 kmlem14 8868 fin23lem24 9027 fin23lem26 9030 fin23lem23 9031 fin23lem22 9032 fin23lem27 9033 ingru 9516 uzin2 13932 incexclem 14407 elrestr 15912 firest 15916 inopn 20529 isbasisg 20562 basis1 20565 basis2 20566 tgval 20570 fctop 20618 cctop 20620 ntrfval 20638 elcls 20687 clsndisj 20689 elcls3 20697 neindisj2 20737 tgrest 20773 restco 20778 restsn 20784 restcld 20786 restcldi 20787 restopnb 20789 neitr 20794 restcls 20795 ordtbaslem 20802 ordtrest2lem 20817 hausnei2 20967 cnhaus 20968 regsep2 20990 dishaus 20996 ordthauslem 20997 cmpsublem 21012 cmpsub 21013 nconsubb 21036 consubclo 21037 1stcelcls 21074 islly 21081 cldllycmp 21108 lly1stc 21109 locfincmp 21139 elkgen 21149 ptclsg 21228 dfac14lem 21230 txrest 21244 pthaus 21251 txhaus 21260 xkohaus 21266 xkoptsub 21267 regr1lem 21352 isfbas 21443 fbasssin 21450 fbun 21454 isfil 21461 fbunfip 21483 fgval 21484 filcon 21497 uzrest 21511 isufil2 21522 hauspwpwf1 21601 fclsopni 21629 fclsnei 21633 fclsrest 21638 fcfnei 21649 fcfneii 21651 tsmsfbas 21741 ustincl 21821 ustdiag 21822 ustinvel 21823 ustexhalf 21824 ust0 21833 trust 21843 restutopopn 21852 lpbl 22118 methaus 22135 metrest 22139 restmetu 22185 qtopbaslem 22372 qdensere 22383 xrtgioo 22417 metnrmlem3 22472 icoopnst 22546 iocopnst 22547 ovolicc2lem2 23093 ovolicc2lem5 23096 mblsplit 23107 limcnlp 23448 ellimc3 23449 limcflf 23451 limciun 23464 ig1pval 23736 shincl 27624 shmodi 27633 omlsi 27647 pjoml 27679 chm0 27734 chincl 27742 chdmm1 27768 ledi 27783 cmbr 27827 cmbr3 27851 mdbr 28537 dmdmd 28543 dmdi 28545 dmdbr3 28548 dmdbr4 28549 mdslmd1lem4 28571 cvmd 28579 cvexch 28617 dmdbr6ati 28666 mddmdin0i 28674 difeq 28739 ofpreima2 28849 ordtrest2NEWlem 29296 inelsros 29568 diffiunisros 29569 measvuni 29604 measinb 29611 inelcarsg 29700 carsgclctunlem2 29708 totprob 29816 ballotlemgval 29912 cvmscbv 30494 cvmsdisj 30506 cvmsss2 30510 nepss 30854 brapply 31215 opnbnd 31490 isfne 31504 tailfb 31542 bj-restsn 32216 bj-restpw 32226 bj-rest0 32227 bj-restb 32228 ptrest 32578 poimirlem30 32609 mblfinlem2 32617 bndss 32755 lcvexchlem4 33342 fipjust 36889 ntrkbimka 37356 ntrk0kbimka 37357 clsk3nimkb 37358 isotone2 37367 ntrclskb 37387 ntrclsk3 37388 ntrclsk13 37389 elrestd 38322 islptre 38686 islpcn 38706 subsaliuncllem 39251 subsaliuncl 39252 nnfoctbdjlem 39348 caragensplit 39390 vonvolmbllem 39550 vonvolmbl 39551 incsmflem 39628 decsmflem 39652 smflimlem2 39658 smflimlem3 39659 smflim 39663 uzlidlring 41719 rngcvalALTV 41753 rngcval 41754 ringcvalALTV 41799 ringcval 41800 |
Copyright terms: Public domain | W3C validator |