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 4120 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) | |
2 | incom 4115 | . 2 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶) | |
3 | incom 4115 | . 2 ⊢ (𝐶 ∩ 𝐵) = (𝐵 ∩ 𝐶) | |
4 | 1, 2, 3 | 3eqtr4g 2803 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1543 ∩ cin 3865 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3070 df-in 3873 |
This theorem is referenced by: ineq12 4122 ineq2i 4124 ineq2d 4127 uneqin 4193 intprgOLD 4895 wefrc 5545 onfr 6252 onnseq 8081 qsdisj 8476 disjenex 8804 fiint 8948 elfiun 9046 dffi3 9047 cplem2 9506 dfac5 9742 kmlem2 9765 kmlem13 9776 kmlem14 9777 ackbij1lem16 9849 fin23lem12 9945 fin23lem19 9950 fin23lem33 9959 uzin2 14908 pgpfac1lem3 19464 pgpfac1lem5 19466 pgpfac1 19467 inopn 21796 basis1 21847 basis2 21848 baspartn 21851 fctop 21901 cctop 21903 ordtbaslem 22085 hausnei2 22250 cnhaus 22251 nrmsep 22254 isnrm2 22255 dishaus 22279 ordthauslem 22280 dfconn2 22316 nconnsubb 22320 finlocfin 22417 dissnlocfin 22426 locfindis 22427 kgeni 22434 pthaus 22535 txhaus 22544 xkohaus 22550 regr1lem 22636 fbasssin 22733 fbun 22737 fbunfip 22766 filconn 22780 isufil2 22805 ufileu 22816 filufint 22817 fmfnfmlem4 22854 fmfnfm 22855 fclsopni 22912 fclsbas 22918 fclsrest 22921 isfcf 22931 tsmsfbas 23025 ustincl 23105 ust0 23117 metreslem 23260 methaus 23418 qtopbaslem 23656 metnrmlem3 23758 ismbl 24423 shincl 29462 chincl 29580 chdmm1 29606 ledi 29621 cmbr 29665 cmbr3i 29681 cmbr3 29689 pjoml2 29692 stcltrlem1 30357 mdbr 30375 dmdbr 30380 cvmd 30417 cvexch 30455 sumdmdii 30496 mddmdin0i 30512 ofpreima2 30723 crefeq 31509 ldgenpisyslem1 31843 ldgenpisys 31846 inelsros 31858 diffiunisros 31859 elcarsg 31984 carsgclctunlem2 31998 carsgclctun 32000 ballotlemfval 32168 ballotlemgval 32202 cvmscbv 32933 cvmsdisj 32945 cvmsss2 32949 satfv1 33038 nepss 33377 tailfb 34303 bj-0int 35007 mblfinlem2 35552 qsdisjALTV 36465 lshpinN 36740 elrfi 40219 fipjust 40848 conrel1d 40948 ntrk0kbimka 41326 clsk3nimkb 41327 isotone2 41336 ntrclskb 41356 ntrclsk3 41357 ntrclsk13 41358 csbresgVD 42188 disjf1 42393 qinioo 42748 fouriersw 43447 nnfoctbdjlem 43668 meadjun 43675 caragenel 43708 sepnsepolem2 45889 sepfsepc 45894 iscnrm3rlem8 45914 iscnrm3llem2 45917 |
Copyright terms: Public domain | W3C validator |