|   | 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 4214 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | |
| 4 | 1, 2, 3 | mp2an 692 | 1 ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷) | 
| Colors of variables: wff setvar class | 
| Syntax hints: = wceq 1539 ∩ cin 3949 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-rab 3436 df-in 3957 | 
| This theorem is referenced by: undir 4286 difundi 4289 difindir 4292 inrab 4315 inrab2 4316 elneldisj 4391 dfif4 4540 dfif5 4541 inxpOLD 5842 resindi 6012 resindir 6013 rnin 6165 inimass 6174 cnvrescnv 6214 predin 6347 funtp 6622 orduniss2 7854 offres 8009 fodomr 9169 fodomfir 9369 epinid0 9641 cnvepnep 9649 wemapwe 9738 cotr3 15018 explecnv 15902 psssdm2 18627 ablfacrp 20087 cnfldfunALT 21380 cnfldfunALTOLD 21393 cnfldfunALTOLDOLD 21394 pjfval2 21730 ofco2 22458 iundisj2 25585 clwwlknondisj 30131 lejdiri 31559 cmbr3i 31620 nonbooli 31671 5oai 31681 3oalem5 31686 mayetes3i 31749 mdexchi 32355 disjpreima 32598 disjxpin 32602 iundisj2f 32604 xppreima 32656 iundisj2fi 32800 xpinpreima 33906 xpinpreima2 33907 ordtcnvNEW 33920 pprodcnveq 35885 dfiota3 35925 bj-inrab 36929 ptrest 37627 ftc1anclem6 37706 xrnres3 38406 br2coss 38440 1cosscnvxrn 38477 refsymrels2 38567 dfeqvrels2 38590 dfeldisj5 38723 dnwech 43065 fgraphopab 43220 onfrALTlem5 44567 onfrALTlem4 44568 onfrALTlem5VD 44910 onfrALTlem4VD 44911 disjxp1 45079 disjinfi 45202 | 
| Copyright terms: Public domain | W3C validator |