| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > elin2 | Structured version Visualization version GIF version | ||
| Description: Membership in a class defined as an intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
| Ref | Expression |
|---|---|
| elin2.x | ⊢ 𝑋 = (𝐵 ∩ 𝐶) |
| Ref | Expression |
|---|---|
| elin2 | ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elin2.x | . . 3 ⊢ 𝑋 = (𝐵 ∩ 𝐶) | |
| 2 | 1 | eleq2i 2833 | . 2 ⊢ (𝐴 ∈ 𝑋 ↔ 𝐴 ∈ (𝐵 ∩ 𝐶)) |
| 3 | elin 3967 | . 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) | |
| 4 | 2, 3 | bitri 275 | 1 ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2108 ∩ cin 3950 |
| 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 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-in 3958 |
| This theorem is referenced by: elin3 4206 opelres 6003 elpredgg 6334 fnres 6695 funfvima 7250 fnwelem 8156 ressuppssdif 8210 fz1isolem 14500 isabl 19802 srhmsubclem1 20677 srhmsubc 20680 isidom 20725 isfld 20740 2idlelb 21263 qus1 21284 qusrhm 21286 lmres 23308 isnvc 24716 cvslvec 25158 cvsclm 25159 iscvs 25160 cvsi 25163 ishl 25396 ply1pid 26222 rplogsum 27571 sltres 27707 iscusgr 29435 isphg 30836 ishlo 30906 hhsscms 31297 mayete3i 31747 isogrp 33079 isofld 33332 bj-elid6 37171 bj-isrvec 37295 caures 37767 iscrngo 38003 fldcrngo 38011 isdmn 38061 isolat 39213 srhmsubcALTV 48241 |
| Copyright terms: Public domain | W3C validator |