| 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 4215 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | |
| 4 | 1, 2, 3 | syl2anc 584 | 1 ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∩ cin 3950 |
| 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-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-in 3958 |
| This theorem is referenced by: csbin 4442 predeq123 6322 funcnvtp 6629 fnunres1 6680 ofrfvalg 7705 offval 7706 oev2 8561 isf32lem7 10399 ressval 17277 invffval 17802 invfval 17803 dfiso2 17816 isofn 17819 oppcinv 17824 zerooval 18040 cat1 18142 isps 18613 dmdprd 20018 dprddisj 20029 dprdf1o 20052 dmdprdsplit2lem 20065 dmdprdpr 20069 pgpfaclem1 20101 isunit 20373 dfrhm2 20474 isrhm 20478 rhmval 20500 2idlval 21261 pjfval 21726 aspval 21893 ressmplbas2 22045 isconn 23421 connsuba 23428 ptbasin 23585 ptclsg 23623 qtopval 23703 rnelfmlem 23960 trust 24238 isnmhm 24767 uniioombllem2a 25617 dyaddisjlem 25630 dyaddisj 25631 i1faddlem 25728 i1fmullem 25729 limcflf 25916 ewlksfval 29619 isewlk 29620 ewlkinedg 29622 ispth 29741 trlsegvdeg 30246 frcond3 30288 numclwwlk3lem2 30403 chocin 31514 cmbr3 31627 pjoml3 31631 fh1 31637 xppreima2 32661 cosnopne 32703 swrdrndisj 32942 hauseqcn 33897 prsssdm 33916 ordtrestNEW 33920 ordtrest2NEW 33922 cndprobval 34435 ballotlemfrc 34529 bnj1421 35056 satffunlem 35406 satffunlem1lem2 35408 satffunlem2lem1 35409 satffunlem2lem2 35411 msrval 35543 msrf 35547 ismfs 35554 clsun 36329 poimirlem8 37635 itg2addnclem2 37679 heiborlem4 37821 heiborlem6 37823 heiborlem10 37827 pmodl42N 39853 polfvalN 39906 poldmj1N 39930 pmapj2N 39931 pnonsingN 39935 psubclinN 39950 poml4N 39955 osumcllem9N 39966 trnfsetN 40157 diainN 41059 djaffvalN 41135 djafvalN 41136 djajN 41139 dihmeetcl 41347 dihmeet2 41348 dochnoncon 41393 djhffval 41398 djhfval 41399 djhlj 41403 dochdmm1 41412 lclkrlem2g 41515 lclkrlem2v 41530 lcfrlem21 41565 lcfrlem24 41568 mapdunirnN 41652 baerlem5amN 41718 baerlem5bmN 41719 baerlem5abmN 41720 mapdheq4lem 41733 mapdh6lem1N 41735 mapdh6lem2N 41736 hdmap1l6lem1 41809 hdmap1l6lem2 41810 aomclem8 43073 disjrnmpt2 45193 dvsinax 45928 dvcosax 45941 nnfoctbdjlem 46470 smfpimcc 46823 smfsuplem2 46827 iscnrm3l 48848 |
| Copyright terms: Public domain | W3C validator |