![]() |
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 4110 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | |
4 | 1, 2, 3 | syl2anc 584 | 1 ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1525 ∩ cin 3864 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-ext 2771 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-rab 3116 df-v 3442 df-in 3872 |
This theorem is referenced by: csbin 4312 predeq123 6031 funcnvtp 6294 offval 7281 ofrfval 7282 oev2 8006 isf32lem7 9634 ressval 16384 invffval 16861 invfval 16862 dfiso2 16875 isofn 16878 oppcinv 16883 zerooval 17092 isps 17645 dmdprd 18841 dprddisj 18852 dprdf1o 18875 dmdprdsplit2lem 18888 dmdprdpr 18892 pgpfaclem1 18924 isunit 19101 dfrhm2 19163 isrhm 19167 2idlval 19699 aspval 19794 ressmplbas2 19927 pjfval 20536 isconn 21709 connsuba 21716 ptbasin 21873 ptclsg 21911 qtopval 21991 rnelfmlem 22248 trust 22525 isnmhm 23042 uniioombllem2a 23870 dyaddisjlem 23883 dyaddisj 23884 i1faddlem 23981 i1fmullem 23982 limcflf 24166 ewlksfval 27070 isewlk 27071 ewlkinedg 27073 ispth 27190 trlsegvdeg 27692 frcond3 27736 numclwwlk3lem2 27851 chocin 28959 cmbr3 29072 pjoml3 29076 fh1 29082 fnunres1 30042 xppreima2 30081 cosnopne 30114 hauseqcn 30751 prsssdm 30773 ordtrestNEW 30777 ordtrest2NEW 30779 cndprobval 31304 ballotlemfrc 31397 bnj1421 31924 satffunlem 32258 satffunlem1lem2 32260 satffunlem2lem1 32261 satffunlem2lem2 32263 msrval 32395 msrf 32399 ismfs 32406 clsun 33287 poimirlem8 34452 itg2addnclem2 34496 heiborlem4 34645 heiborlem6 34647 heiborlem10 34651 pmodl42N 36539 polfvalN 36592 poldmj1N 36616 pmapj2N 36617 pnonsingN 36621 psubclinN 36636 poml4N 36641 osumcllem9N 36652 trnfsetN 36843 diainN 37745 djaffvalN 37821 djafvalN 37822 djajN 37825 dihmeetcl 38033 dihmeet2 38034 dochnoncon 38079 djhffval 38084 djhfval 38085 djhlj 38089 dochdmm1 38098 lclkrlem2g 38201 lclkrlem2v 38216 lcfrlem21 38251 lcfrlem24 38254 mapdunirnN 38338 baerlem5amN 38404 baerlem5bmN 38405 baerlem5abmN 38406 mapdheq4lem 38419 mapdh6lem1N 38421 mapdh6lem2N 38422 hdmap1l6lem1 38495 hdmap1l6lem2 38496 aomclem8 39167 disjrnmpt2 41010 dvsinax 41760 dvcosax 41774 nnfoctbdjlem 42301 smfpimcc 42646 smfsuplem2 42650 rhmval 43690 |
Copyright terms: Public domain | W3C validator |