MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elin2 Structured version   Unicode version

Theorem elin2 3538
Description: Membership in a class defined as an intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.)
Hypothesis
Ref Expression
elin2.x  |-  X  =  ( B  i^i  C
)
Assertion
Ref Expression
elin2  |-  ( A  e.  X  <->  ( A  e.  B  /\  A  e.  C ) )

Proof of Theorem elin2
StepHypRef Expression
1 elin2.x . . 3  |-  X  =  ( B  i^i  C
)
21eleq2i 2505 . 2  |-  ( A  e.  X  <->  A  e.  ( B  i^i  C ) )
3 elin 3536 . 2  |-  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) )
42, 3bitri 249 1  |-  ( A  e.  X  <->  ( A  e.  B  /\  A  e.  C ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    = wceq 1364    e. wcel 1761    i^i cin 3324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-in 3332
This theorem is referenced by:  elin3  3539  fnres  5524  funfvima  5949  fnwelem  6686  ressuppssdif  6709  fz1isolem  12210  isabl  16274  isfld  16821  2idlcpbl  17294  divs1  17295  divsrhm  17297  isidom  17354  lmres  18804  isnvc  20175  cvslvec  20578  cvsclm  20579  ishl  20774  ply1pid  21594  rplogsum  22719  isphg  24136  ishlo  24207  hhsscms  24599  mayete3i  25050  isogrp  26082  isofld  26189  elpredim  27550  elpred  27551  elpredg  27552  sltres  27718  nofulllem5  27760  caures  28565  iscrngo  28706  fldcrng  28713  isdmn  28763  isolat  32545
  Copyright terms: Public domain W3C validator