![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ineq12d | Structured version Visualization version GIF version |
Description: Equality deduction for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Ref | Expression |
---|---|
ineq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
ineq12d.2 | ⊢ (𝜑 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
ineq12d | ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ineq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | ineq12d.2 | . 2 ⊢ (𝜑 → 𝐶 = 𝐷) | |
3 | ineq12 4207 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | |
4 | 1, 2, 3 | syl2anc 583 | 1 ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1540 ∩ cin 3947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1543 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3432 df-in 3955 |
This theorem is referenced by: csbin 4439 predeq123 6301 funcnvtp 6611 fnunres1 6661 ofrfvalg 7682 offval 7683 oev2 8529 isf32lem7 10360 ressval 17183 invffval 17712 invfval 17713 dfiso2 17726 isofn 17729 oppcinv 17734 zerooval 17955 cat1 18057 isps 18531 dmdprd 19916 dprddisj 19927 dprdf1o 19950 dmdprdsplit2lem 19963 dmdprdpr 19967 pgpfaclem1 19999 isunit 20271 dfrhm2 20372 isrhm 20376 rhmval 20398 2idlval 21096 pjfval 21571 aspval 21737 ressmplbas2 21893 isconn 23237 connsuba 23244 ptbasin 23401 ptclsg 23439 qtopval 23519 rnelfmlem 23776 trust 24054 isnmhm 24583 uniioombllem2a 25431 dyaddisjlem 25444 dyaddisj 25445 i1faddlem 25542 i1fmullem 25543 limcflf 25730 ewlksfval 29292 isewlk 29293 ewlkinedg 29295 ispth 29414 trlsegvdeg 29914 frcond3 29956 numclwwlk3lem2 30071 chocin 31182 cmbr3 31295 pjoml3 31299 fh1 31305 xppreima2 32310 cosnopne 32350 swrdrndisj 32555 hauseqcn 33343 prsssdm 33362 ordtrestNEW 33366 ordtrest2NEW 33368 cndprobval 33897 ballotlemfrc 33990 bnj1421 34518 satffunlem 34857 satffunlem1lem2 34859 satffunlem2lem1 34860 satffunlem2lem2 34862 msrval 34994 msrf 34998 ismfs 35005 clsun 35679 poimirlem8 36962 itg2addnclem2 37006 heiborlem4 37148 heiborlem6 37150 heiborlem10 37154 pmodl42N 39188 polfvalN 39241 poldmj1N 39265 pmapj2N 39266 pnonsingN 39270 psubclinN 39285 poml4N 39290 osumcllem9N 39301 trnfsetN 39492 diainN 40394 djaffvalN 40470 djafvalN 40471 djajN 40474 dihmeetcl 40682 dihmeet2 40683 dochnoncon 40728 djhffval 40733 djhfval 40734 djhlj 40738 dochdmm1 40747 lclkrlem2g 40850 lclkrlem2v 40865 lcfrlem21 40900 lcfrlem24 40903 mapdunirnN 40987 baerlem5amN 41053 baerlem5bmN 41054 baerlem5abmN 41055 mapdheq4lem 41068 mapdh6lem1N 41070 mapdh6lem2N 41071 hdmap1l6lem1 41144 hdmap1l6lem2 41145 aomclem8 42268 disjrnmpt2 44348 dvsinax 45090 dvcosax 45103 nnfoctbdjlem 45632 smfpimcc 45985 smfsuplem2 45989 iscnrm3l 47748 |
Copyright terms: Public domain | W3C validator |