| 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 4213 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) | |
| 2 | incom 4209 | . 2 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶) | |
| 3 | incom 4209 | . 2 ⊢ (𝐶 ∩ 𝐵) = (𝐵 ∩ 𝐶) | |
| 4 | 1, 2, 3 | 3eqtr4g 2802 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∩ cin 3950 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-in 3958 |
| This theorem is referenced by: ineq12 4215 ineq2i 4217 ineq2d 4220 uneqin 4289 wefrc 5679 onfr 6423 onnseq 8384 qsdisj 8834 disjenex 9175 fiint 9366 fiintOLD 9367 elfiun 9470 dffi3 9471 cplem2 9930 dfac5 10169 kmlem2 10192 kmlem13 10203 kmlem14 10204 ackbij1lem16 10274 fin23lem12 10371 fin23lem19 10376 fin23lem33 10385 uzin2 15383 pgpfac1lem3 20097 pgpfac1lem5 20099 pgpfac1 20100 inopn 22905 basis1 22957 basis2 22958 baspartn 22961 fctop 23011 cctop 23013 ordtbaslem 23196 hausnei2 23361 cnhaus 23362 nrmsep 23365 isnrm2 23366 dishaus 23390 ordthauslem 23391 dfconn2 23427 nconnsubb 23431 finlocfin 23528 dissnlocfin 23537 locfindis 23538 kgeni 23545 pthaus 23646 txhaus 23655 xkohaus 23661 regr1lem 23747 fbasssin 23844 fbun 23848 fbunfip 23877 filconn 23891 isufil2 23916 ufileu 23927 filufint 23928 fmfnfmlem4 23965 fmfnfm 23966 fclsopni 24023 fclsbas 24029 fclsrest 24032 isfcf 24042 tsmsfbas 24136 ustincl 24216 ust0 24228 metreslem 24372 methaus 24533 qtopbaslem 24779 metnrmlem3 24883 ismbl 25561 shincl 31400 chincl 31518 chdmm1 31544 ledi 31559 cmbr 31603 cmbr3i 31619 cmbr3 31627 pjoml2 31630 stcltrlem1 32295 mdbr 32313 dmdbr 32318 cvmd 32355 cvexch 32393 sumdmdii 32434 mddmdin0i 32450 ofpreima2 32676 ssdifidllem 33484 ssdifidl 33485 ssdifidlprm 33486 1arithufdlem4 33575 crefeq 33844 ldgenpisyslem1 34164 ldgenpisys 34167 inelsros 34179 diffiunisros 34180 elcarsg 34307 carsgclctunlem2 34321 carsgclctun 34323 ballotlemfval 34492 ballotlemgval 34526 cvmscbv 35263 cvmsdisj 35275 cvmsss2 35279 satfv1 35368 nepss 35718 tailfb 36378 bj-0int 37102 mblfinlem2 37665 qsdisjALTV 38616 lshpinN 38990 elrfi 42705 fipjust 43578 conrel1d 43676 ntrk0kbimka 44052 clsk3nimkb 44053 isotone2 44062 ntrclskb 44082 ntrclsk3 44083 ntrclsk13 44084 csbresgVD 44915 wfac8prim 45019 disjf1 45188 qinioo 45548 fouriersw 46246 nnfoctbdjlem 46470 meadjun 46477 caragenel 46510 sepnsepolem2 48820 sepfsepc 48825 iscnrm3rlem8 48844 iscnrm3llem2 48847 |
| Copyright terms: Public domain | W3C validator |