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 3419 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐶} = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐶}) | |
2 | dfin5 3896 | . 2 ⊢ (𝐴 ∩ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐶} | |
3 | dfin5 3896 | . 2 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐶} | |
4 | 1, 2, 3 | 3eqtr4g 2804 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2107 {crab 3069 ∩ cin 3887 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2710 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1783 df-sb 2069 df-clab 2717 df-cleq 2731 df-clel 2817 df-rab 3074 df-in 3895 |
This theorem is referenced by: ineq2 4141 ineq12 4142 ineq1i 4143 ineq1d 4146 unineq 4212 dfrab3ss 4247 disjeq0 4390 intprgOLD 4916 inex1g 5244 reseq1 5888 sspred 6215 isofrlem 7220 qsdisj 8592 fiint 9100 elfiun 9198 dffi3 9199 inf3lema 9391 dfac5lem5 9892 kmlem12 9926 kmlem14 9928 fin23lem24 10087 fin23lem26 10090 fin23lem23 10091 fin23lem22 10092 fin23lem27 10093 ingru 10580 uzin2 15065 incexclem 15557 elrestr 17148 firest 17152 inopn 22057 isbasisg 22106 basis1 22109 basis2 22110 tgval 22114 fctop 22163 cctop 22165 ntrfval 22184 elcls 22233 clsndisj 22235 elcls3 22243 neindisj2 22283 tgrest 22319 restco 22324 restsn 22330 restcld 22332 restcldi 22333 restopnb 22335 neitr 22340 restcls 22341 ordtbaslem 22348 ordtrest2lem 22363 hausnei2 22513 cnhaus 22514 regsep2 22536 dishaus 22542 ordthauslem 22543 cmpsublem 22559 cmpsub 22560 nconnsubb 22583 connsubclo 22584 1stcelcls 22621 islly 22628 cldllycmp 22655 lly1stc 22656 locfincmp 22686 elkgen 22696 ptclsg 22775 dfac14lem 22777 txrest 22791 pthaus 22798 txhaus 22807 xkohaus 22813 xkoptsub 22814 regr1lem 22899 isfbas 22989 fbasssin 22996 fbun 23000 isfil 23007 fbunfip 23029 fgval 23030 filconn 23043 uzrest 23057 isufil2 23068 hauspwpwf1 23147 fclsopni 23175 fclsnei 23179 fclsrest 23184 fcfnei 23195 fcfneii 23197 tsmsfbas 23288 ustincl 23368 ustdiag 23369 ustinvel 23370 ustexhalf 23371 ust0 23380 trust 23390 restutopopn 23399 lpbl 23668 methaus 23685 metrest 23689 restmetu 23735 qtopbaslem 23931 qdensere 23942 xrtgioo 23978 metnrmlem3 24033 icoopnst 24111 iocopnst 24112 ovolicc2lem2 24691 ovolicc2lem5 24694 mblsplit 24705 limcnlp 25051 ellimc3 25052 limcflf 25054 limciun 25067 ig1pval 25346 shincl 29752 shmodi 29761 omlsi 29775 pjoml 29807 chm0 29862 chincl 29870 chdmm1 29896 ledi 29911 cmbr 29955 cmbr3 29979 mdbr 30665 dmdmd 30671 dmdi 30673 dmdbr3 30676 dmdbr4 30677 mdslmd1lem4 30699 cvmd 30707 cvexch 30745 dmdbr6ati 30794 mddmdin0i 30802 difeq 30874 ofpreima2 31012 rspectopn 31826 ordtrest2NEWlem 31881 inelsros 32155 diffiunisros 32156 measvuni 32191 measinb 32198 inelcarsg 32287 carsgclctunlem2 32295 totprob 32403 ballotlemgval 32499 cvmscbv 33229 cvmsdisj 33241 cvmsss2 33245 satfv1 33334 nepss 33671 brapply 34249 opnbnd 34523 isfne 34537 tailfb 34575 bj-restsn 35262 bj-restpw 35272 bj-rest0 35273 bj-restb 35274 nlpfvineqsn 35589 fvineqsnf1 35590 pibt2 35597 ptrest 35785 poimirlem30 35816 mblfinlem2 35824 bndss 35953 qsdisjALTV 36735 redundss3 36748 lcvexchlem4 37058 fipjust 41179 ntrkbimka 41655 ntrk0kbimka 41656 clsk3nimkb 41657 isotone2 41666 ntrclskb 41686 ntrclsk3 41687 ntrclsk13 41688 ismnushort 41926 elrestd 42665 islptre 43167 islpcn 43187 subsaliuncllem 43903 subsaliuncl 43904 nnfoctbdjlem 44000 caragensplit 44045 vonvolmbllem 44205 vonvolmbl 44206 incsmflem 44286 decsmflem 44311 smflimlem2 44317 smflimlem3 44318 smflim 44322 smfpimcclem 44351 uzlidlring 45498 rngcvalALTV 45530 rngcval 45531 ringcvalALTV 45576 ringcval 45577 sepfsepc 46232 iscnrm3rlem2 46246 iscnrm3rlem8 46252 iscnrm3llem2 46255 |
Copyright terms: Public domain | W3C validator |