|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > ineq12 | Structured version Visualization version GIF version | ||
| Description: Equality theorem for intersection of two classes. (Contributed by NM, 8-May-1994.) | 
| Ref | Expression | 
|---|---|
| ineq12 | ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | ineq1 4213 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) | |
| 2 | ineq2 4214 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | |
| 3 | 1, 2 | sylan9eq 2797 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∩ cin 3950 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-in 3958 | 
| This theorem is referenced by: ineq12i 4218 ineq12d 4221 ineqan12d 4222 fnun 6682 frrlem4 8314 undifixp 8974 endisj 9098 sbthlem8 9130 fiin 9462 pm54.43 10041 kmlem9 10199 indistopon 23008 epttop 23016 restbas 23166 ordtbas2 23199 txbas 23575 ptbasin 23585 trfbas2 23851 snfil 23872 fbasrn 23892 trfil2 23895 fmfnfmlem3 23964 ustuqtop2 24251 minveclem3b 25462 isperp 28720 brredunds 38627 diophin 42783 kelac2lem 43076 iscnrm3r 48845 | 
| Copyright terms: Public domain | W3C validator |