| 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 4172 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) | |
| 2 | ineq2 4173 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | |
| 3 | 1, 2 | sylan9eq 2784 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∩ cin 3910 |
| 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 2008 ax-8 2111 ax-9 2119 ax-ext 2701 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2721 df-clel 2803 df-rab 3403 df-in 3918 |
| This theorem is referenced by: ineq12i 4177 ineq12d 4180 ineqan12d 4181 fnun 6614 frrlem4 8245 undifixp 8884 endisj 9005 sbthlem8 9035 fiin 9349 pm54.43 9930 kmlem9 10088 indistopon 22864 epttop 22872 restbas 23021 ordtbas2 23054 txbas 23430 ptbasin 23440 trfbas2 23706 snfil 23727 fbasrn 23747 trfil2 23750 fmfnfmlem3 23819 ustuqtop2 24106 minveclem3b 25304 isperp 28615 brredunds 38590 diophin 42733 kelac2lem 43026 iscnrm3r 48909 incat 49563 setc1onsubc 49564 |
| Copyright terms: Public domain | W3C validator |