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

Theorem elini 4208
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 3978 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
41, 2, 3mpbir2an 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