![]() |
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 4630 | . 2 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1632 ∩ cint 4627 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-ral 3055 df-int 4628 |
This theorem is referenced by: intprg 4663 elreldm 5505 ordintdif 5935 fniinfv 6420 onsucmin 7187 elxp5 7277 1stval2 7351 2ndval2 7352 fundmen 8197 xpsnen 8211 unblem2 8380 unblem3 8381 fiint 8404 elfi2 8487 fi0 8493 elfiun 8503 tcvalg 8789 tz9.12lem3 8827 rankvalb 8835 rankvalg 8855 ranksnb 8865 rankonidlem 8866 cardval3 8988 cardidm 8995 cfval 9281 cflim3 9296 coftr 9307 isfin3ds 9363 fin23lem17 9372 fin23lem39 9384 isf33lem 9400 isf34lem5 9412 isf34lem6 9414 wuncval 9776 tskmval 9873 cleq1 13943 dfrtrcl2 14021 mrcfval 16490 mrcval 16492 cycsubg2 17852 efgval 18350 lspfval 19195 lspval 19197 lsppropd 19240 aspval 19550 aspval2 19569 clsfval 21051 clsval 21063 clsval2 21076 hauscmplem 21431 cmpfi 21433 1stcfb 21470 fclscmp 22055 spanval 28522 chsupid 28601 sigagenval 30533 kur14 31526 mclsval 31788 scutval 32238 igenval 34191 pclfvalN 35696 pclvalN 35697 diaintclN 36867 docaffvalN 36930 docafvalN 36931 docavalN 36932 dibintclN 36976 dihglb2 37151 dihintcl 37153 mzpval 37815 dnnumch3lem 38136 aomclem8 38151 rgspnval 38258 iotain 39138 salgenval 41062 |
Copyright terms: Public domain | W3C validator |