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 3769 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) | |
2 | incom 3767 | . 2 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶) | |
3 | incom 3767 | . 2 ⊢ (𝐶 ∩ 𝐵) = (𝐵 ∩ 𝐶) | |
4 | 1, 2, 3 | 3eqtr4g 2669 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ∩ 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: ineq12 3771 ineq2i 3773 ineq2d 3776 uneqin 3837 intprg 4446 wefrc 5032 onfr 5680 onnseq 7328 qsdisj 7711 disjenex 8003 fiint 8122 elfiun 8219 dffi3 8220 cplem2 8636 dfac5 8834 kmlem2 8856 kmlem13 8867 kmlem14 8868 ackbij1lem16 8940 fin23lem12 9036 fin23lem19 9041 fin23lem33 9050 uzin2 13932 pgpfac1lem3 18299 pgpfac1lem5 18301 pgpfac1 18302 inopn 20529 basis1 20565 basis2 20566 baspartn 20569 fctop 20618 cctop 20620 ordtbaslem 20802 hausnei2 20967 cnhaus 20968 nrmsep 20971 isnrm2 20972 dishaus 20996 ordthauslem 20997 dfcon2 21032 nconsubb 21036 finlocfin 21133 dissnlocfin 21142 locfindis 21143 kgeni 21150 pthaus 21251 txhaus 21260 xkohaus 21266 regr1lem 21352 fbasssin 21450 fbun 21454 fbunfip 21483 filcon 21497 isufil2 21522 ufileu 21533 filufint 21534 fmfnfmlem4 21571 fmfnfm 21572 fclsopni 21629 fclsbas 21635 fclsrest 21638 isfcf 21648 tsmsfbas 21741 ustincl 21821 ust0 21833 metreslem 21977 methaus 22135 qtopbaslem 22372 metnrmlem3 22472 ismbl 23101 shincl 27624 chincl 27742 chdmm1 27768 ledi 27783 cmbr 27827 cmbr3i 27843 cmbr3 27851 pjoml2 27854 stcltrlem1 28519 mdbr 28537 dmdbr 28542 cvmd 28579 cvexch 28617 sumdmdii 28658 mddmdin0i 28674 ofpreima2 28849 crefeq 29240 ldgenpisyslem1 29553 ldgenpisys 29556 inelsros 29568 diffiunisros 29569 elcarsg 29694 carsgclctunlem2 29708 carsgclctun 29710 ballotlemfval 29878 ballotlemgval 29912 cvmscbv 30494 cvmsdisj 30506 cvmsss2 30510 nepss 30854 tailfb 31542 mblfinlem2 32617 lshpinN 33294 elrfi 36275 fipjust 36889 conrel1d 36974 ntrk0kbimka 37357 clsk3nimkb 37358 isotone2 37367 ntrclskb 37387 ntrclsk3 37388 ntrclsk13 37389 csbresgVD 38153 disjf1 38364 qinioo 38609 fouriersw 39124 nnfoctbdjlem 39348 meadjun 39355 caragenel 39385 |
Copyright terms: Public domain | W3C validator |