| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > ineq1 | GIF version | ||
| Description: Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.) |
| Ref | Expression |
|---|---|
| ineq1 | ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleq2 2269 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
| 2 | 1 | anbi1d 465 | . . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))) |
| 3 | elin 3356 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶)) | |
| 4 | elin 3356 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) | |
| 5 | 2, 3, 4 | 3bitr4g 223 | . 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ 𝑥 ∈ (𝐵 ∩ 𝐶))) |
| 6 | 5 | eqrdv 2203 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∧ wa 104 = wceq 1373 ∈ wcel 2176 ∩ cin 3165 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-ext 2187 |
| This theorem depends on definitions: df-bi 117 df-tru 1376 df-nf 1484 df-sb 1786 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-v 2774 df-in 3172 |
| This theorem is referenced by: ineq2 3368 ineq12 3369 ineq1i 3370 ineq1d 3373 dfrab3ss 3451 intprg 3918 inex1g 4180 reseq1 4953 fiintim 7028 uzin2 11298 ressvalsets 12896 elrestr 13079 tgval 13094 inopn 14475 isbasisg 14516 basis1 14519 basis2 14520 ntrfval 14572 tgrest 14641 restco 14646 restsn 14652 restopnb 14653 txrest 14748 metrest 14978 qtopbasss 14993 bdinex1g 15837 |
| Copyright terms: Public domain | W3C validator |