MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elini Structured version   Visualization version   GIF version

Theorem elini 4154
Description: Membership in an intersection of two classes. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
elini.1 𝐴𝐵
elini.2 𝐴𝐶
Assertion
Ref Expression
elini 𝐴 ∈ (𝐵𝐶)

Proof of Theorem elini
StepHypRef Expression
1 elini.1 . 2 𝐴𝐵
2 elini.2 . 2 𝐴𝐶
3 elin 3935 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
41, 2, 3mpbir2an 710 1 𝐴 ∈ (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wcel 2115  cin 3918
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-in 3926
This theorem is referenced by:  isfin1-3  9800  isdrs2  17545  fpwipodrs  17770  0cmp  21995  comppfsc  22133  ptcmpfi  22414  alexsubALTlem2  22649  alexsubALTlem4  22651  ptcmp  22659  cnstrcvs  23742  cncvs  23746  recvs  23747  qcvs  23748  cnncvs  23760  ovolicc1  24116  ioorf  24173  corclrcl  40261  0pwfi  41550  sge0rnn0  42870  sge0reuz  42949
  Copyright terms: Public domain W3C validator