![]() |
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 3952 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | |
4 | 1, 2, 3 | syl2anc 696 | 1 ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1632 ∩ cin 3714 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-v 3342 df-in 3722 |
This theorem is referenced by: csbin 4153 predeq123 5842 funprgOLD 6102 funtpgOLD 6104 funcnvtp 6112 offval 7069 ofrfval 7070 oev2 7772 isf32lem7 9373 ressval 16129 invffval 16619 invfval 16620 dfiso2 16633 isofn 16636 oppcinv 16641 zerooval 16850 isps 17403 dmdprd 18597 dprddisj 18608 dprdf1o 18631 dmdprdsplit2lem 18644 dmdprdpr 18648 pgpfaclem1 18680 isunit 18857 dfrhm2 18919 isrhm 18923 2idlval 19435 aspval 19530 ressmplbas2 19657 pjfval 20252 isconn 21418 connsuba 21425 ptbasin 21582 ptclsg 21620 qtopval 21700 rnelfmlem 21957 trust 22234 isnmhm 22751 uniioombllem2a 23550 dyaddisjlem 23563 dyaddisj 23564 i1faddlem 23659 i1fmullem 23660 limcflf 23844 ewlksfval 26707 isewlk 26708 ewlkinedg 26710 ispth 26829 trlsegvdeg 27379 frcond3 27423 numclwwlk3lem 27552 chocin 28663 cmbr3 28776 pjoml3 28780 fh1 28786 fnunres1 29724 xppreima2 29759 hauseqcn 30250 prsssdm 30272 ordtrestNEW 30276 ordtrest2NEW 30278 cndprobval 30804 ballotlemfrc 30897 bnj1421 31417 msrval 31742 msrf 31746 ismfs 31753 clsun 32629 poimirlem8 33730 itg2addnclem2 33775 heiborlem4 33926 heiborlem6 33928 heiborlem10 33932 pmodl42N 35640 polfvalN 35693 poldmj1N 35717 pmapj2N 35718 pnonsingN 35722 psubclinN 35737 poml4N 35742 osumcllem9N 35753 trnfsetN 35945 diainN 36848 djaffvalN 36924 djafvalN 36925 djajN 36928 dihmeetcl 37136 dihmeet2 37137 dochnoncon 37182 djhffval 37187 djhfval 37188 djhlj 37192 dochdmm1 37201 lclkrlem2g 37304 lclkrlem2v 37319 lcfrlem21 37354 lcfrlem24 37357 mapdunirnN 37441 baerlem5amN 37507 baerlem5bmN 37508 baerlem5abmN 37509 mapdheq4lem 37522 mapdh6lem1N 37524 mapdh6lem2N 37525 hdmap1l6lem1 37599 hdmap1l6lem2 37600 aomclem8 38133 csbingOLD 39554 disjrnmpt2 39874 dvsinax 40630 dvcosax 40644 nnfoctbdjlem 41175 smfpimcc 41520 smfsuplem2 41524 rhmval 42429 |
Copyright terms: Public domain | W3C validator |