![]() |
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 2818 | . 2 ⊢ (𝐴 ∈ 𝑋 ↔ 𝐴 ∈ (𝐵 ∩ 𝐶)) |
3 | elin 3963 | . 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) | |
4 | 2, 3 | bitri 274 | 1 ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 394 = wceq 1534 ∈ wcel 2099 ∩ cin 3946 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3465 df-in 3954 |
This theorem is referenced by: elin3 4199 opelres 5986 elpredgg 6316 fnres 6678 funfvima 7237 fnwelem 8135 ressuppssdif 8189 fz1isolem 14473 isabl 19776 srhmsubclem1 20649 srhmsubc 20652 isidom 20697 isfld 20712 2idlelb 21236 qus1 21257 qusrhm 21259 lmres 23290 isnvc 24698 cvslvec 25138 cvsclm 25139 iscvs 25140 cvsi 25143 ishl 25376 ply1pid 26205 rplogsum 27551 sltres 27687 iscusgr 29349 isphg 30745 ishlo 30815 hhsscms 31206 mayete3i 31656 isogrp 32939 isofld 33183 bj-elid6 36888 bj-isrvec 37012 caures 37472 iscrngo 37708 fldcrngo 37716 isdmn 37766 isolat 38921 srhmsubcALTV 47736 |
Copyright terms: Public domain | W3C validator |