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 3769 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) | |
2 | ineq2 3770 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | |
3 | 1, 2 | sylan9eq 2664 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1475 ∩ cin 3539 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-in 3547 |
This theorem is referenced by: ineq12i 3774 ineq12d 3777 ineqan12d 3778 fnun 5911 undifixp 7830 endisj 7932 sbthlem8 7962 fiin 8211 pm54.43 8709 kmlem9 8863 indistopon 20615 epttop 20623 restbas 20772 ordtbas2 20805 txbas 21180 ptbasin 21190 trfbas2 21457 snfil 21478 fbasrn 21498 trfil2 21501 fmfnfmlem3 21570 ustuqtop2 21856 minveclem3b 23007 isperp 25407 frrlem4 31027 diophin 36354 kelac2lem 36652 |
Copyright terms: Public domain | W3C validator |