| 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 22921 epttop 22929 restbas 23078 ordtbas2 23111 txbas 23487 ptbasin 23497 trfbas2 23763 snfil 23784 fbasrn 23804 trfil2 23807 fmfnfmlem3 23876 ustuqtop2 24163 minveclem3b 25361 isperp 28692 brredunds 38610 diophin 42753 kelac2lem 43046 iscnrm3r 48929 incat 49583 setc1onsubc 49584 |
| Copyright terms: Public domain | W3C validator |