![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elini | Structured version Visualization version GIF version |
Description: Membership in an intersection of two classes. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Ref | Expression |
---|---|
elini.1 | ⊢ 𝐴 ∈ 𝐵 |
elini.2 | ⊢ 𝐴 ∈ 𝐶 |
Ref | Expression |
---|---|
elini | ⊢ 𝐴 ∈ (𝐵 ∩ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elini.1 | . 2 ⊢ 𝐴 ∈ 𝐵 | |
2 | elini.2 | . 2 ⊢ 𝐴 ∈ 𝐶 | |
3 | elin 3978 | . 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) | |
4 | 1, 2, 3 | mpbir2an 711 | 1 ⊢ 𝐴 ∈ (𝐵 ∩ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 ∩ cin 3961 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1539 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-v 3479 df-in 3969 |
This theorem is referenced by: isfin1-3 10423 setc2ohom 18148 isdrs2 18363 fpwipodrs 18597 0cmp 23417 comppfsc 23555 ptcmpfi 23836 alexsubALTlem2 24071 alexsubALTlem4 24073 ptcmp 24081 cnstrcvs 25187 cncvs 25191 recvs 25192 recvsOLD 25193 qcvs 25194 cnncvs 25206 ovolicc1 25564 ioorf 25621 zringpid 33559 corclrcl 43696 0pwfi 44998 sge0rnn0 46323 sge0reuz 46402 |
Copyright terms: Public domain | W3C validator |