| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > inteqd | Structured version Visualization version GIF version | ||
| Description: Equality deduction for class intersection. (Contributed by NM, 2-Sep-2003.) |
| Ref | Expression |
|---|---|
| inteqd.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
| Ref | Expression |
|---|---|
| inteqd | ⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | inteqd.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 2 | inteq 4949 | . 2 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∩ cint 4946 |
| 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-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-ral 3062 df-rex 3071 df-int 4947 |
| This theorem is referenced by: elreldm 5946 ordintdif 6434 fniinfv 6987 onsucmin 7841 elxp5 7945 1stval2 8031 2ndval2 8032 naddcllem 8714 naddov2 8717 naddcom 8720 naddrid 8721 naddasslem1 8732 naddasslem2 8733 naddass 8734 naddsuc2 8739 fundmen 9071 xpsnen 9095 unblem2 9329 unblem3 9330 fiint 9366 fiintOLD 9367 elfi2 9454 fi0 9460 elfiun 9470 tcvalg 9778 tz9.12lem3 9829 rankvalb 9837 rankvalg 9857 ranksnb 9867 rankonidlem 9868 cardval3 9992 cardidm 9999 harsucnn 10038 cfval 10287 cflim3 10302 coftr 10313 isfin3ds 10369 fin23lem17 10378 fin23lem39 10390 isf33lem 10406 isf34lem5 10418 isf34lem6 10420 wuncval 10782 tskmval 10879 cleq1 15022 dfrtrcl2 15101 mrcfval 17651 mrcval 17653 cycsubg2 19228 efgval 19735 rgspnval 20612 lspfval 20971 lspval 20973 lsppropd 21017 aspval 21893 aspval2 21918 clsfval 23033 clsval 23045 clsval2 23058 hauscmplem 23414 cmpfi 23416 1stcfb 23453 fclscmp 24038 scutval 27845 spanval 31352 chsupid 31431 intimafv 32720 fldgenval 33314 primefldgen1 33323 zarclsint 33871 zarcmplem 33880 sigagenval 34141 kur14 35221 mclsval 35568 igenval 38068 pclfvalN 39891 pclvalN 39892 diaintclN 41060 docaffvalN 41123 docafvalN 41124 docavalN 41125 dibintclN 41169 dihglb2 41344 dihintcl 41346 mzpval 42743 dnnumch3lem 43058 aomclem8 43073 rp-intrabeq 43233 nadd1suc 43405 minregex2 43548 iotain 44436 salgenval 46336 mreclat 48886 |
| Copyright terms: Public domain | W3C validator |