Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ineq2 | Structured version Visualization version GIF version |
Description: Equality theorem for intersection of two classes. (Contributed by NM, 26-Dec-1993.) |
Ref | Expression |
---|---|
ineq2 | ⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ineq1 4180 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) | |
2 | incom 4177 | . 2 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶) | |
3 | incom 4177 | . 2 ⊢ (𝐶 ∩ 𝐵) = (𝐵 ∩ 𝐶) | |
4 | 1, 2, 3 | 3eqtr4g 2881 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ∩ cin 3934 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-tru 1531 df-ex 1772 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-rab 3147 df-in 3942 |
This theorem is referenced by: ineq12 4183 ineq2i 4185 ineq2d 4188 uneqin 4254 intprg 4903 wefrc 5543 onfr 6224 onnseq 7972 qsdisj 8364 disjenex 8664 fiint 8784 elfiun 8883 dffi3 8884 cplem2 9308 dfac5 9543 kmlem2 9566 kmlem13 9577 kmlem14 9578 ackbij1lem16 9646 fin23lem12 9742 fin23lem19 9747 fin23lem33 9756 uzin2 14694 pgpfac1lem3 19130 pgpfac1lem5 19132 pgpfac1 19133 inopn 21437 basis1 21488 basis2 21489 baspartn 21492 fctop 21542 cctop 21544 ordtbaslem 21726 hausnei2 21891 cnhaus 21892 nrmsep 21895 isnrm2 21896 dishaus 21920 ordthauslem 21921 dfconn2 21957 nconnsubb 21961 finlocfin 22058 dissnlocfin 22067 locfindis 22068 kgeni 22075 pthaus 22176 txhaus 22185 xkohaus 22191 regr1lem 22277 fbasssin 22374 fbun 22378 fbunfip 22407 filconn 22421 isufil2 22446 ufileu 22457 filufint 22458 fmfnfmlem4 22495 fmfnfm 22496 fclsopni 22553 fclsbas 22559 fclsrest 22562 isfcf 22572 tsmsfbas 22665 ustincl 22745 ust0 22757 metreslem 22901 methaus 23059 qtopbaslem 23296 metnrmlem3 23398 ismbl 24056 shincl 29086 chincl 29204 chdmm1 29230 ledi 29245 cmbr 29289 cmbr3i 29305 cmbr3 29313 pjoml2 29316 stcltrlem1 29981 mdbr 29999 dmdbr 30004 cvmd 30041 cvexch 30079 sumdmdii 30120 mddmdin0i 30136 ofpreima2 30340 crefeq 31009 ldgenpisyslem1 31322 ldgenpisys 31325 inelsros 31337 diffiunisros 31338 elcarsg 31463 carsgclctunlem2 31477 carsgclctun 31479 ballotlemfval 31647 ballotlemgval 31681 cvmscbv 32403 cvmsdisj 32415 cvmsss2 32419 satfv1 32508 nepss 32846 tailfb 33623 bj-0int 34288 mblfinlem2 34812 qsdisjALTV 35732 lshpinN 36007 elrfi 39171 fipjust 39804 conrel1d 39888 ntrk0kbimka 40269 clsk3nimkb 40270 isotone2 40279 ntrclskb 40299 ntrclsk3 40300 ntrclsk13 40301 csbresgVD 41109 disjf1 41323 qinioo 41691 fouriersw 42397 nnfoctbdjlem 42618 meadjun 42625 caragenel 42658 |
Copyright terms: Public domain | W3C validator |