![]() |
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 4204 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) | |
2 | incom 4200 | . 2 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶) | |
3 | incom 4200 | . 2 ⊢ (𝐶 ∩ 𝐵) = (𝐵 ∩ 𝐶) | |
4 | 1, 2, 3 | 3eqtr4g 2797 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 ∩ cin 3946 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-rab 3433 df-in 3954 |
This theorem is referenced by: ineq12 4206 ineq2i 4208 ineq2d 4211 uneqin 4277 intprgOLD 4987 wefrc 5669 onfr 6400 onnseq 8340 qsdisj 8784 disjenex 9131 fiint 9320 elfiun 9421 dffi3 9422 cplem2 9881 dfac5 10119 kmlem2 10142 kmlem13 10153 kmlem14 10154 ackbij1lem16 10226 fin23lem12 10322 fin23lem19 10327 fin23lem33 10336 uzin2 15287 pgpfac1lem3 19941 pgpfac1lem5 19943 pgpfac1 19944 inopn 22392 basis1 22444 basis2 22445 baspartn 22448 fctop 22498 cctop 22500 ordtbaslem 22683 hausnei2 22848 cnhaus 22849 nrmsep 22852 isnrm2 22853 dishaus 22877 ordthauslem 22878 dfconn2 22914 nconnsubb 22918 finlocfin 23015 dissnlocfin 23024 locfindis 23025 kgeni 23032 pthaus 23133 txhaus 23142 xkohaus 23148 regr1lem 23234 fbasssin 23331 fbun 23335 fbunfip 23364 filconn 23378 isufil2 23403 ufileu 23414 filufint 23415 fmfnfmlem4 23452 fmfnfm 23453 fclsopni 23510 fclsbas 23516 fclsrest 23519 isfcf 23529 tsmsfbas 23623 ustincl 23703 ust0 23715 metreslem 23859 methaus 24020 qtopbaslem 24266 metnrmlem3 24368 ismbl 25034 shincl 30621 chincl 30739 chdmm1 30765 ledi 30780 cmbr 30824 cmbr3i 30840 cmbr3 30848 pjoml2 30851 stcltrlem1 31516 mdbr 31534 dmdbr 31539 cvmd 31576 cvexch 31614 sumdmdii 31655 mddmdin0i 31671 ofpreima2 31878 crefeq 32813 ldgenpisyslem1 33149 ldgenpisys 33152 inelsros 33164 diffiunisros 33165 elcarsg 33292 carsgclctunlem2 33306 carsgclctun 33308 ballotlemfval 33476 ballotlemgval 33510 cvmscbv 34237 cvmsdisj 34249 cvmsss2 34253 satfv1 34342 nepss 34675 tailfb 35250 bj-0int 35970 mblfinlem2 36514 qsdisjALTV 37473 lshpinN 37847 elrfi 41417 fipjust 42301 conrel1d 42399 ntrk0kbimka 42775 clsk3nimkb 42776 isotone2 42785 ntrclskb 42805 ntrclsk3 42806 ntrclsk13 42807 csbresgVD 43641 disjf1 43865 qinioo 44234 fouriersw 44933 nnfoctbdjlem 45157 meadjun 45164 caragenel 45197 sepnsepolem2 47508 sepfsepc 47513 iscnrm3rlem8 47533 iscnrm3llem2 47536 |
Copyright terms: Public domain | W3C validator |