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 4098 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | |
4 | 1, 2, 3 | syl2anc 587 | 1 ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∩ cin 3842 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-rab 3062 df-in 3850 |
This theorem is referenced by: csbin 4329 predeq123 6130 funcnvtp 6402 ofrfvalg 7432 offval 7433 oev2 8179 isf32lem7 9859 ressval 16654 invffval 17133 invfval 17134 dfiso2 17147 isofn 17150 oppcinv 17155 zerooval 17367 cat1 17469 isps 17928 dmdprd 19239 dprddisj 19250 dprdf1o 19273 dmdprdsplit2lem 19286 dmdprdpr 19290 pgpfaclem1 19322 isunit 19529 dfrhm2 19591 isrhm 19595 2idlval 20125 pjfval 20522 aspval 20686 ressmplbas2 20838 isconn 22164 connsuba 22171 ptbasin 22328 ptclsg 22366 qtopval 22446 rnelfmlem 22703 trust 22981 isnmhm 23499 uniioombllem2a 24334 dyaddisjlem 24347 dyaddisj 24348 i1faddlem 24445 i1fmullem 24446 limcflf 24633 ewlksfval 27543 isewlk 27544 ewlkinedg 27546 ispth 27664 trlsegvdeg 28164 frcond3 28206 numclwwlk3lem2 28321 chocin 29430 cmbr3 29543 pjoml3 29547 fh1 29553 fnunres1 30519 xppreima2 30562 cosnopne 30602 swrdrndisj 30804 hauseqcn 31420 prsssdm 31439 ordtrestNEW 31443 ordtrest2NEW 31445 cndprobval 31970 ballotlemfrc 32063 bnj1421 32593 satffunlem 32934 satffunlem1lem2 32936 satffunlem2lem1 32937 satffunlem2lem2 32939 msrval 33071 msrf 33075 ismfs 33082 clsun 34155 poimirlem8 35408 itg2addnclem2 35452 heiborlem4 35595 heiborlem6 35597 heiborlem10 35601 pmodl42N 37488 polfvalN 37541 poldmj1N 37565 pmapj2N 37566 pnonsingN 37570 psubclinN 37585 poml4N 37590 osumcllem9N 37601 trnfsetN 37792 diainN 38694 djaffvalN 38770 djafvalN 38771 djajN 38774 dihmeetcl 38982 dihmeet2 38983 dochnoncon 39028 djhffval 39033 djhfval 39034 djhlj 39038 dochdmm1 39047 lclkrlem2g 39150 lclkrlem2v 39165 lcfrlem21 39200 lcfrlem24 39203 mapdunirnN 39287 baerlem5amN 39353 baerlem5bmN 39354 baerlem5abmN 39355 mapdheq4lem 39368 mapdh6lem1N 39370 mapdh6lem2N 39371 hdmap1l6lem1 39444 hdmap1l6lem2 39445 aomclem8 40458 disjrnmpt2 42264 dvsinax 42996 dvcosax 43009 nnfoctbdjlem 43535 smfpimcc 43880 smfsuplem2 43884 rhmval 45011 iscnrm3l 45767 |
Copyright terms: Public domain | W3C validator |