![]() |
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 4752 | . 2 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 ∩ cint 4749 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-ext 2751 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-sb 2016 df-clab 2760 df-cleq 2772 df-clel 2847 df-ral 3094 df-int 4750 |
This theorem is referenced by: intprg 4783 elreldm 5648 ordintdif 6078 fniinfv 6570 onsucmin 7352 elxp5 7443 1stval2 7518 2ndval2 7519 fundmen 8380 xpsnen 8397 unblem2 8566 unblem3 8567 fiint 8590 elfi2 8673 fi0 8679 elfiun 8689 tcvalg 8974 tz9.12lem3 9012 rankvalb 9020 rankvalg 9040 ranksnb 9050 rankonidlem 9051 cardval3 9175 cardidm 9182 cfval 9467 cflim3 9482 coftr 9493 isfin3ds 9549 fin23lem17 9558 fin23lem39 9570 isf33lem 9586 isf34lem5 9598 isf34lem6 9600 wuncval 9962 tskmval 10059 cleq1 14204 dfrtrcl2 14282 mrcfval 16737 mrcval 16739 cycsubg2 18100 efgval 18601 lspfval 19467 lspval 19469 lsppropd 19512 aspval 19822 aspval2 19841 clsfval 21337 clsval 21349 clsval2 21362 hauscmplem 21718 cmpfi 21720 1stcfb 21757 fclscmp 22342 spanval 28891 chsupid 28970 sigagenval 31041 kur14 32045 mclsval 32327 scutval 32783 igenval 34778 pclfvalN 36467 pclvalN 36468 diaintclN 37636 docaffvalN 37699 docafvalN 37700 docavalN 37701 dibintclN 37745 dihglb2 37920 dihintcl 37922 mzpval 38721 dnnumch3lem 39039 aomclem8 39054 rgspnval 39161 iotain 40163 salgenval 42035 |
Copyright terms: Public domain | W3C validator |