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 4142 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | |
4 | 1, 2, 3 | syl2anc 584 | 1 ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∩ cin 3887 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2710 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2069 df-clab 2717 df-cleq 2731 df-clel 2817 df-rab 3074 df-in 3895 |
This theorem is referenced by: csbin 4374 predeq123 6207 funcnvtp 6504 ofrfvalg 7550 offval 7551 oev2 8362 isf32lem7 10124 ressval 16953 invffval 17479 invfval 17480 dfiso2 17493 isofn 17496 oppcinv 17501 zerooval 17719 cat1 17821 isps 18295 dmdprd 19610 dprddisj 19621 dprdf1o 19644 dmdprdsplit2lem 19657 dmdprdpr 19661 pgpfaclem1 19693 isunit 19908 dfrhm2 19970 isrhm 19974 2idlval 20513 pjfval 20922 aspval 21086 ressmplbas2 21237 isconn 22573 connsuba 22580 ptbasin 22737 ptclsg 22775 qtopval 22855 rnelfmlem 23112 trust 23390 isnmhm 23919 uniioombllem2a 24755 dyaddisjlem 24768 dyaddisj 24769 i1faddlem 24866 i1fmullem 24867 limcflf 25054 ewlksfval 27977 isewlk 27978 ewlkinedg 27980 ispth 28100 trlsegvdeg 28600 frcond3 28642 numclwwlk3lem2 28757 chocin 29866 cmbr3 29979 pjoml3 29983 fh1 29989 fnunres1 30954 xppreima2 30997 cosnopne 31036 swrdrndisj 31238 hauseqcn 31857 prsssdm 31876 ordtrestNEW 31880 ordtrest2NEW 31882 cndprobval 32409 ballotlemfrc 32502 bnj1421 33031 satffunlem 33372 satffunlem1lem2 33374 satffunlem2lem1 33375 satffunlem2lem2 33377 msrval 33509 msrf 33513 ismfs 33520 clsun 34526 poimirlem8 35794 itg2addnclem2 35838 heiborlem4 35981 heiborlem6 35983 heiborlem10 35987 pmodl42N 37872 polfvalN 37925 poldmj1N 37949 pmapj2N 37950 pnonsingN 37954 psubclinN 37969 poml4N 37974 osumcllem9N 37985 trnfsetN 38176 diainN 39078 djaffvalN 39154 djafvalN 39155 djajN 39158 dihmeetcl 39366 dihmeet2 39367 dochnoncon 39412 djhffval 39417 djhfval 39418 djhlj 39422 dochdmm1 39431 lclkrlem2g 39534 lclkrlem2v 39549 lcfrlem21 39584 lcfrlem24 39587 mapdunirnN 39671 baerlem5amN 39737 baerlem5bmN 39738 baerlem5abmN 39739 mapdheq4lem 39752 mapdh6lem1N 39754 mapdh6lem2N 39755 hdmap1l6lem1 39828 hdmap1l6lem2 39829 aomclem8 40893 disjrnmpt2 42733 dvsinax 43461 dvcosax 43474 nnfoctbdjlem 44000 smfpimcc 44352 smfsuplem2 44356 rhmval 45488 iscnrm3l 46256 |
Copyright terms: Public domain | W3C validator |