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

Theorem elin2 3623
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 2523 . 2  |-  ( A  e.  X  <->  A  e.  ( B  i^i  C ) )
3 elin 3619 . 2  |-  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) )
42, 3bitri 253 1  |-  ( A  e.  X  <->  ( A  e.  B  /\  A  e.  C ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    /\ wa 371    = wceq 1446    e. wcel 1889    i^i cin 3405
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-v 3049  df-in 3413
This theorem is referenced by:  elin3  3626  elpredim  5395  elpred  5396  elpredg  5397  fnres  5697  funfvima  6145  fnwelem  6916  ressuppssdif  6941  fz1isolem  12631  isabl  17446  isfld  17996  2idlcpbl  18470  qus1  18471  qusrhm  18473  isidom  18540  lmres  20328  isnvc  21709  cvslvec  22149  cvsclm  22150  ishl  22341  ply1pid  23149  rplogsum  24377  isphg  26470  ishlo  26551  hhsscms  26942  mayete3i  27393  isogrp  28477  isofld  28577  sltres  30563  nofulllem5  30607  caures  32101  iscrngo  32242  fldcrng  32249  isdmn  32299  isolat  32790  srhmsubclem1  40179  srhmsubc  40182  srhmsubcALTVlem1  40198  srhmsubcALTV  40201
  Copyright terms: Public domain W3C validator