![]() |
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 3424 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐶} = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐶}) | |
2 | dfin5 3923 | . 2 ⊢ (𝐴 ∩ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐶} | |
3 | dfin5 3923 | . 2 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐶} | |
4 | 1, 2, 3 | 3eqtr4g 2802 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2107 {crab 3410 ∩ cin 3914 |
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 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-rab 3411 df-in 3922 |
This theorem is referenced by: ineq2 4171 ineq12 4172 ineq1i 4173 ineq1d 4176 unineq 4242 dfrab3ss 4277 disjeq0 4420 intprgOLD 4950 inex1g 5281 reseq1 5936 sspred 6267 isofrlem 7290 qsdisj 8740 fiint 9275 elfiun 9373 dffi3 9374 inf3lema 9567 dfac5lem5 10070 kmlem12 10104 kmlem14 10106 fin23lem24 10265 fin23lem26 10268 fin23lem23 10269 fin23lem22 10270 fin23lem27 10271 ingru 10758 uzin2 15236 incexclem 15728 elrestr 17317 firest 17321 inopn 22264 isbasisg 22313 basis1 22316 basis2 22317 tgval 22321 fctop 22370 cctop 22372 ntrfval 22391 elcls 22440 clsndisj 22442 elcls3 22450 neindisj2 22490 tgrest 22526 restco 22531 restsn 22537 restcld 22539 restcldi 22540 restopnb 22542 neitr 22547 restcls 22548 ordtbaslem 22555 ordtrest2lem 22570 hausnei2 22720 cnhaus 22721 regsep2 22743 dishaus 22749 ordthauslem 22750 cmpsublem 22766 cmpsub 22767 nconnsubb 22790 connsubclo 22791 1stcelcls 22828 islly 22835 cldllycmp 22862 lly1stc 22863 locfincmp 22893 elkgen 22903 ptclsg 22982 dfac14lem 22984 txrest 22998 pthaus 23005 txhaus 23014 xkohaus 23020 xkoptsub 23021 regr1lem 23106 isfbas 23196 fbasssin 23203 fbun 23207 isfil 23214 fbunfip 23236 fgval 23237 filconn 23250 uzrest 23264 isufil2 23275 hauspwpwf1 23354 fclsopni 23382 fclsnei 23386 fclsrest 23391 fcfnei 23402 fcfneii 23404 tsmsfbas 23495 ustincl 23575 ustdiag 23576 ustinvel 23577 ustexhalf 23578 ust0 23587 trust 23597 restutopopn 23606 lpbl 23875 methaus 23892 metrest 23896 restmetu 23942 qtopbaslem 24138 qdensere 24149 xrtgioo 24185 metnrmlem3 24240 icoopnst 24318 iocopnst 24319 ovolicc2lem2 24898 ovolicc2lem5 24901 mblsplit 24912 limcnlp 25258 ellimc3 25259 limcflf 25261 limciun 25274 ig1pval 25553 shincl 30365 shmodi 30374 omlsi 30388 pjoml 30420 chm0 30475 chincl 30483 chdmm1 30509 ledi 30524 cmbr 30568 cmbr3 30592 mdbr 31278 dmdmd 31284 dmdi 31286 dmdbr3 31289 dmdbr4 31290 mdslmd1lem4 31312 cvmd 31320 cvexch 31358 dmdbr6ati 31407 mddmdin0i 31415 difeq 31487 ofpreima2 31624 rspectopn 32488 ordtrest2NEWlem 32543 inelsros 32817 diffiunisros 32818 measvuni 32853 measinb 32860 inelcarsg 32951 carsgclctunlem2 32959 totprob 33067 ballotlemgval 33163 cvmscbv 33892 cvmsdisj 33904 cvmsss2 33908 satfv1 33997 nepss 34329 brapply 34552 opnbnd 34826 isfne 34840 tailfb 34878 bj-restsn 35582 bj-restpw 35592 bj-rest0 35593 bj-restb 35594 nlpfvineqsn 35909 fvineqsnf1 35910 pibt2 35917 ptrest 36106 poimirlem30 36137 mblfinlem2 36145 bndss 36274 qsdisjALTV 37106 redundss3 37119 lcvexchlem4 37528 fipjust 41911 ntrkbimka 42384 ntrk0kbimka 42385 clsk3nimkb 42386 isotone2 42395 ntrclskb 42415 ntrclsk3 42416 ntrclsk13 42417 ismnushort 42655 elrestd 43392 restsubel 43442 islptre 43934 islpcn 43954 subsaliuncllem 44672 subsaliuncl 44673 nnfoctbdjlem 44770 caragensplit 44815 vonvolmbllem 44975 vonvolmbl 44976 incsmflem 45056 decsmflem 45081 smflimlem2 45087 smflimlem3 45088 smflim 45092 smfpimcclem 45122 uzlidlring 46301 rngcvalALTV 46333 rngcval 46334 ringcvalALTV 46379 ringcval 46380 sepfsepc 47034 iscnrm3rlem2 47048 iscnrm3rlem8 47054 iscnrm3llem2 47057 |
Copyright terms: Public domain | W3C validator |