![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ineq12i | Structured version Visualization version GIF version |
Description: Equality inference for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
Ref | Expression |
---|---|
ineq1i.1 | ⊢ 𝐴 = 𝐵 |
ineq12i.2 | ⊢ 𝐶 = 𝐷 |
Ref | Expression |
---|---|
ineq12i | ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ineq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | ineq12i.2 | . 2 ⊢ 𝐶 = 𝐷 | |
3 | ineq12 4168 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | |
4 | 1, 2, 3 | mp2an 691 | 1 ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ∩ cin 3910 |
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 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3407 df-in 3918 |
This theorem is referenced by: undir 4237 difundi 4240 difindir 4243 inrab 4267 inrab2 4268 elneldisj 4349 dfif4 4502 dfif5 4503 inxp 5789 resindi 5954 resindir 5955 rnin 6100 inimass 6108 cnvrescnv 6148 predin 6282 funtp 6559 orduniss2 7769 offres 7917 fodomr 9075 epinid0 9541 cnvepnep 9549 wemapwe 9638 cotr3 14869 explecnv 15755 psssdm2 18475 ablfacrp 19850 cnfldfunALT 20825 cnfldfunALTOLD 20826 pjfval2 21131 ofco2 21816 iundisj2 24929 clwwlknondisj 29097 lejdiri 30523 cmbr3i 30584 nonbooli 30635 5oai 30645 3oalem5 30650 mayetes3i 30713 mdexchi 31319 disjpreima 31548 disjxpin 31552 iundisj2f 31554 xppreima 31608 iundisj2fi 31747 xpinpreima 32544 xpinpreima2 32545 ordtcnvNEW 32558 pprodcnveq 34514 dfiota3 34554 bj-inrab 35443 ptrest 36123 ftc1anclem6 36202 xrnres3 36912 br2coss 36946 1cosscnvxrn 36983 refsymrels2 37073 dfeqvrels2 37096 dfeldisj5 37229 dnwech 41418 fgraphopab 41580 onfrALTlem5 42912 onfrALTlem4 42913 onfrALTlem5VD 43255 onfrALTlem4VD 43256 disjxp1 43365 disjinfi 43500 |
Copyright terms: Public domain | W3C validator |