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

Theorem elin2 3359
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 2347 . 2  |-  ( A  e.  X  <->  A  e.  ( B  i^i  C ) )
3 elin 3358 . 2  |-  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) )
42, 3bitri 240 1  |-  ( A  e.  X  <->  ( A  e.  B  /\  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    = wceq 1623    e. wcel 1684    i^i cin 3151
This theorem is referenced by:  elin3  3360  fnres  5360  funfvima  5753  fnwelem  6230  fz1isolem  11399  isabl  15093  isfld  15521  2idlcpbl  15986  divs1  15987  divsrhm  15989  isidom  16045  lmres  17028  isnvc  18205  ishl  18779  ply1pid  19565  rplogsum  20676  isphg  21395  ishlo  21466  hhsscms  21856  mayete3i  22307  elpredim  24176  elpred  24177  elpredg  24178  sltres  24318  nofulllem5  24360  caures  26476  iscrngo  26622  fldcrng  26629  isdmn  26679  isolat  29402
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159
  Copyright terms: Public domain W3C validator