Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ineq12d | Structured version Visualization version Unicode 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 3809 | . 2 | |
4 | 1, 2, 3 | syl2anc 693 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1483 cin 3573 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-in 3581 |
This theorem is referenced by: csbin 4010 predeq123 5681 funprgOLD 5941 funtpgOLD 5943 funcnvtp 5951 offval 6904 ofrfval 6905 oev2 7603 isf32lem7 9181 ressval 15927 invffval 16418 invfval 16419 dfiso2 16432 isofn 16435 oppcinv 16440 zerooval 16649 isps 17202 dmdprd 18397 dprddisj 18408 dprdf1o 18431 dmdprdsplit2lem 18444 dmdprdpr 18448 pgpfaclem1 18480 isunit 18657 dfrhm2 18717 isrhm 18721 2idlval 19233 aspval 19328 ressmplbas2 19455 pjfval 20050 isconn 21216 connsuba 21223 ptbasin 21380 ptclsg 21418 qtopval 21498 rnelfmlem 21756 trust 22033 isnmhm 22550 uniioombllem2a 23350 dyaddisjlem 23363 dyaddisj 23364 i1faddlem 23460 i1fmullem 23461 limcflf 23645 ewlksfval 26497 isewlk 26498 ewlkinedg 26500 ispth 26619 trlsegvdeg 27087 frcond3 27133 chocin 28354 cmbr3 28467 pjoml3 28471 fh1 28477 fnunres1 29417 xppreima2 29450 hauseqcn 29941 prsssdm 29963 ordtrestNEW 29967 ordtrest2NEW 29969 cndprobval 30495 ballotlemfrc 30588 bnj1421 31110 msrval 31435 msrf 31439 ismfs 31446 clsun 32323 poimirlem8 33417 itg2addnclem2 33462 heiborlem4 33613 heiborlem6 33615 heiborlem10 33619 pmodl42N 35137 polfvalN 35190 poldmj1N 35214 pmapj2N 35215 pnonsingN 35219 psubclinN 35234 poml4N 35239 osumcllem9N 35250 trnfsetN 35442 diainN 36346 djaffvalN 36422 djafvalN 36423 djajN 36426 dihmeetcl 36634 dihmeet2 36635 dochnoncon 36680 djhffval 36685 djhfval 36686 djhlj 36690 dochdmm1 36699 lclkrlem2g 36802 lclkrlem2v 36817 lcfrlem21 36852 lcfrlem24 36855 mapdunirnN 36939 baerlem5amN 37005 baerlem5bmN 37006 baerlem5abmN 37007 mapdheq4lem 37020 mapdh6lem1N 37022 mapdh6lem2N 37023 hdmap1l6lem1 37097 hdmap1l6lem2 37098 aomclem8 37631 csbingOLD 39054 disjrnmpt2 39375 dvsinax 40127 dvcosax 40141 nnfoctbdjlem 40672 smfpimcc 41014 smfsuplem2 41018 rhmval 41919 |
Copyright terms: Public domain | W3C validator |