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 4872 | . 2 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ∩ cint 4869 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-ral 3143 df-int 4870 |
This theorem is referenced by: intprg 4903 elreldm 5799 ordintdif 6234 fniinfv 6736 onsucmin 7524 elxp5 7616 1stval2 7697 2ndval2 7698 fundmen 8572 xpsnen 8590 unblem2 8760 unblem3 8761 fiint 8784 elfi2 8867 fi0 8873 elfiun 8883 tcvalg 9169 tz9.12lem3 9207 rankvalb 9215 rankvalg 9235 ranksnb 9245 rankonidlem 9246 cardval3 9370 cardidm 9377 cfval 9658 cflim3 9673 coftr 9684 isfin3ds 9740 fin23lem17 9749 fin23lem39 9761 isf33lem 9777 isf34lem5 9789 isf34lem6 9791 wuncval 10153 tskmval 10250 cleq1 14333 dfrtrcl2 14411 mrcfval 16869 mrcval 16871 cycsubg2 18293 efgval 18774 lspfval 19676 lspval 19678 lsppropd 19721 aspval 20032 aspval2 20057 clsfval 21563 clsval 21575 clsval2 21588 hauscmplem 21944 cmpfi 21946 1stcfb 21983 fclscmp 22568 spanval 29038 chsupid 29117 sigagenval 31299 kur14 32361 mclsval 32708 scutval 33163 igenval 35222 pclfvalN 36907 pclvalN 36908 diaintclN 38076 docaffvalN 38139 docafvalN 38140 docavalN 38141 dibintclN 38185 dihglb2 38360 dihintcl 38362 mzpval 39209 dnnumch3lem 39526 aomclem8 39541 rgspnval 39648 harsucnn 39783 iotain 40629 salgenval 42487 |
Copyright terms: Public domain | W3C validator |