![]() |
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 2874 | . 2 ⊢ (𝐴 ∈ 𝑋 ↔ 𝐴 ∈ (𝐵 ∩ 𝐶)) |
3 | elin 4094 | . 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) | |
4 | 2, 3 | bitri 276 | 1 ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 = wceq 1522 ∈ wcel 2081 ∩ cin 3862 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-v 3439 df-in 3870 |
This theorem is referenced by: elin3 4102 opelres 5745 elpredim 6040 elpred 6041 elpredg 6042 fnres 6349 funfvima 6863 fnwelem 7683 ressuppssdif 7707 fz1isolem 13672 isabl 18642 isfld 19206 2idlcpbl 19701 qus1 19702 qusrhm 19704 isidom 19771 lmres 21597 isnvc 22992 cvslvec 23417 cvsclm 23418 iscvs 23419 cvsi 23422 ishl 23653 ply1pid 24461 rplogsum 25790 iscusgr 26888 isphg 28290 ishlo 28360 hhsscms 28751 mayete3i 29201 isogrp 30368 isofld 30534 sltres 32784 caures 34592 iscrngo 34831 fldcrng 34839 isdmn 34889 isolat 35904 srhmsubclem1 43848 srhmsubc 43851 srhmsubcALTV 43869 |
Copyright terms: Public domain | W3C validator |