| 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.) (Proof shortened by SN, 20-Sep-2023.) |
| Ref | Expression |
|---|---|
| ineq1 | ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rabeq 3451 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐶} = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐶}) | |
| 2 | dfin5 3959 | . 2 ⊢ (𝐴 ∩ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐶} | |
| 3 | dfin5 3959 | . 2 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐶} | |
| 4 | 1, 2, 3 | 3eqtr4g 2802 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 {crab 3436 ∩ 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-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: ineq2 4214 ineq12 4215 ineq1i 4216 ineq1d 4219 unineq 4288 dfrab3ss 4323 disjeq0 4456 inex1g 5319 reseq1 5991 sspred 6330 isofrlem 7360 qsdisj 8834 fiint 9366 fiintOLD 9367 elfiun 9470 dffi3 9471 inf3lema 9664 dfac5lem5 10167 kmlem12 10202 kmlem14 10204 fin23lem24 10362 fin23lem26 10365 fin23lem23 10366 fin23lem22 10367 fin23lem27 10368 ingru 10855 uzin2 15383 incexclem 15872 elrestr 17473 firest 17477 rngcval 20618 ringcval 20647 inopn 22905 isbasisg 22954 basis1 22957 basis2 22958 tgval 22962 fctop 23011 cctop 23013 ntrfval 23032 elcls 23081 clsndisj 23083 elcls3 23091 neindisj2 23131 tgrest 23167 restco 23172 restsn 23178 restcld 23180 restcldi 23181 restopnb 23183 neitr 23188 restcls 23189 ordtbaslem 23196 ordtrest2lem 23211 hausnei2 23361 cnhaus 23362 regsep2 23384 dishaus 23390 ordthauslem 23391 cmpsublem 23407 cmpsub 23408 nconnsubb 23431 connsubclo 23432 1stcelcls 23469 islly 23476 cldllycmp 23503 lly1stc 23504 locfincmp 23534 elkgen 23544 ptclsg 23623 dfac14lem 23625 txrest 23639 pthaus 23646 txhaus 23655 xkohaus 23661 xkoptsub 23662 regr1lem 23747 isfbas 23837 fbasssin 23844 fbun 23848 isfil 23855 fbunfip 23877 fgval 23878 filconn 23891 uzrest 23905 isufil2 23916 hauspwpwf1 23995 fclsopni 24023 fclsnei 24027 fclsrest 24032 fcfnei 24043 fcfneii 24045 tsmsfbas 24136 ustincl 24216 ustdiag 24217 ustinvel 24218 ustexhalf 24219 ust0 24228 trust 24238 restutopopn 24247 lpbl 24516 methaus 24533 metrest 24537 restmetu 24583 qtopbaslem 24779 qdensere 24790 xrtgioo 24828 metnrmlem3 24883 icoopnst 24969 iocopnst 24970 ovolicc2lem2 25553 ovolicc2lem5 25556 mblsplit 25567 limcnlp 25913 ellimc3 25914 limcflf 25916 limciun 25929 ig1pval 26215 shincl 31400 shmodi 31409 omlsi 31423 pjoml 31455 chm0 31510 chincl 31518 chdmm1 31544 ledi 31559 cmbr 31603 cmbr3 31627 mdbr 32313 dmdmd 32319 dmdi 32321 dmdbr3 32324 dmdbr4 32325 mdslmd1lem4 32347 cvmd 32355 cvexch 32393 dmdbr6ati 32442 mddmdin0i 32450 difeq 32537 ofpreima2 32676 ssdifidlprm 33486 ufdprmidl 33569 1arithufdlem4 33575 rspectopn 33866 ordtrest2NEWlem 33921 inelsros 34179 diffiunisros 34180 measvuni 34215 measinb 34222 inelcarsg 34313 carsgclctunlem2 34321 totprob 34429 ballotlemgval 34526 cvmscbv 35263 cvmsdisj 35275 cvmsss2 35279 satfv1 35368 nepss 35718 brapply 35939 opnbnd 36326 isfne 36340 tailfb 36378 bj-restsn 37083 bj-restpw 37093 bj-rest0 37094 bj-restb 37095 nlpfvineqsn 37410 fvineqsnf1 37411 pibt2 37418 ptrest 37626 poimirlem30 37657 mblfinlem2 37665 bndss 37793 qsdisjALTV 38616 redundss3 38629 lcvexchlem4 39038 fipjust 43578 ntrkbimka 44051 ntrk0kbimka 44052 clsk3nimkb 44053 isotone2 44062 ntrclskb 44082 ntrclsk3 44083 ntrclsk13 44084 ismnushort 44320 relpfrlem 44974 elrestd 45113 restsubel 45158 islptre 45634 islpcn 45654 subsaliuncllem 46372 subsaliuncl 46373 nnfoctbdjlem 46470 caragensplit 46515 vonvolmbllem 46675 vonvolmbl 46676 incsmflem 46756 decsmflem 46781 smflimlem2 46787 smflimlem3 46788 smflim 46792 smfpimcclem 46822 uzlidlring 48151 rngcvalALTV 48181 ringcvalALTV 48205 sepfsepc 48825 iscnrm3rlem2 48838 iscnrm3rlem8 48844 iscnrm3llem2 48847 |
| Copyright terms: Public domain | W3C validator |