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

Theorem elin2 3653
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 2500 . 2  |-  ( A  e.  X  <->  A  e.  ( B  i^i  C ) )
3 elin 3649 . 2  |-  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) )
42, 3bitri 252 1  |-  ( A  e.  X  <->  ( A  e.  B  /\  A  e.  C ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1868    i^i cin 3435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-v 3083  df-in 3443
This theorem is referenced by:  elin3  3654  elpredim  5408  elpred  5409  elpredg  5410  fnres  5707  funfvima  6152  fnwelem  6919  ressuppssdif  6944  fz1isolem  12622  isabl  17422  isfld  17972  2idlcpbl  18446  qus1  18447  qusrhm  18449  isidom  18516  lmres  20303  isnvc  21684  cvslvec  22124  cvsclm  22125  ishl  22316  ply1pid  23124  rplogsum  24352  isphg  26444  ishlo  26525  hhsscms  26916  mayete3i  27367  isogrp  28460  isofld  28561  sltres  30546  nofulllem5  30588  caures  32003  iscrngo  32144  fldcrng  32151  isdmn  32201  isolat  32697  srhmsubclem1  39347  srhmsubc  39350  srhmsubcALTVlem1  39366  srhmsubcALTV  39369
  Copyright terms: Public domain W3C validator