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

Theorem elin2 3629
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 2480 . 2  |-  ( A  e.  X  <->  A  e.  ( B  i^i  C ) )
3 elin 3625 . 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 367    = wceq 1405    e. wcel 1842    i^i cin 3412
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3060  df-in 3420
This theorem is referenced by:  elin3  3630  elpredim  5378  elpred  5379  elpredg  5380  fnres  5677  funfvima  6127  fnwelem  6898  ressuppssdif  6923  fz1isolem  12557  isabl  17124  isfld  17723  2idlcpbl  18200  qus1  18201  qusrhm  18203  isidom  18271  lmres  20092  isnvc  21493  cvslvec  21896  cvsclm  21897  ishl  22092  ply1pid  22870  rplogsum  24091  isphg  26132  ishlo  26203  hhsscms  26595  mayete3i  27046  isogrp  28130  isofld  28231  sltres  30111  nofulllem5  30153  caures  31515  iscrngo  31656  fldcrng  31663  isdmn  31713  isolat  32210  srhmsubclem1  38373  srhmsubc  38376  srhmsubcALTVlem1  38392  srhmsubcALTV  38395
  Copyright terms: Public domain W3C validator