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

Theorem elin2 3652
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 2532 . 2  |-  ( A  e.  X  <->  A  e.  ( B  i^i  C ) )
3 elin 3650 . 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 1370    e. wcel 1758    i^i cin 3438
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-in 3446
This theorem is referenced by:  elin3  3653  fnres  5638  funfvima  6064  fnwelem  6800  ressuppssdif  6823  fz1isolem  12336  isabl  16406  isfld  16974  2idlcpbl  17449  divs1  17450  divsrhm  17452  isidom  17509  lmres  19046  isnvc  20417  cvslvec  20820  cvsclm  20821  ishl  21016  ply1pid  21794  rplogsum  22919  isphg  24396  ishlo  24467  hhsscms  24859  mayete3i  25310  isogrp  26337  isofld  26438  elpredim  27804  elpred  27805  elpredg  27806  sltres  27972  nofulllem5  28014  caures  28827  iscrngo  28968  fldcrng  28975  isdmn  29025  isolat  33220
  Copyright terms: Public domain W3C validator