![]() |
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 3842 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | |
4 | 1, 2, 3 | mp2an 708 | 1 ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1523 ∩ cin 3606 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-v 3233 df-in 3614 |
This theorem is referenced by: undir 3909 difundi 3912 difindir 3915 inrab 3932 inrab2 3933 elneldisj 3996 elneldisjOLD 3998 dfif4 4134 dfif5 4135 inxp 5287 resindi 5447 resindir 5448 rnin 5577 inimass 5584 predin 5741 funtp 5983 orduniss2 7075 offres 7205 fodomr 8152 wemapwe 8632 cotr3 13763 explecnv 14641 psssdm2 17262 ablfacrp 18511 cnfldfun 19806 pjfval2 20101 ofco2 20305 iundisj2 23363 clwwlknondisj 27086 lejdiri 28526 cmbr3i 28587 nonbooli 28638 5oai 28648 3oalem5 28653 mayetes3i 28716 mdexchi 29322 disjpreima 29523 disjxpin 29527 iundisj2f 29529 xppreima 29577 iundisj2fi 29684 xpinpreima 30080 xpinpreima2 30081 ordtcnvNEW 30094 pprodcnveq 32115 dfiota3 32155 bj-inrab 33048 ptrest 33538 ftc1anclem6 33620 xrnres3 34302 br2coss 34333 1cosscnvxrn 34365 refsymrels2 34449 dnwech 37935 fgraphopab 38105 onfrALTlem5 39074 onfrALTlem4 39075 onfrALTlem5VD 39435 onfrALTlem4VD 39436 disjxp1 39552 disjinfi 39694 |
Copyright terms: Public domain | W3C validator |