![]() |
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 4030 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) | |
2 | ineq2 4031 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | |
3 | 1, 2 | sylan9eq 2834 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 = wceq 1601 ∩ cin 3791 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-v 3400 df-in 3799 |
This theorem is referenced by: ineq12i 4035 ineq12d 4038 ineqan12d 4039 fnun 6243 undifixp 8230 endisj 8335 sbthlem8 8365 fiin 8616 pm54.43 9159 kmlem9 9315 indistopon 21213 epttop 21221 restbas 21370 ordtbas2 21403 txbas 21779 ptbasin 21789 trfbas2 22055 snfil 22076 fbasrn 22096 trfil2 22099 fmfnfmlem3 22168 ustuqtop2 22454 minveclem3b 23634 isperp 26063 frrlem4 32372 brreds 34997 diophin 38300 kelac2lem 38597 |
Copyright terms: Public domain | W3C validator |