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

Theorem elin2 4196
Description: Membership in a class defined as an intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.)
Hypothesis
Ref Expression
elin2.x 𝑋 = (𝐵𝐶)
Assertion
Ref Expression
elin2 (𝐴𝑋 ↔ (𝐴𝐵𝐴𝐶))

Proof of Theorem elin2
StepHypRef Expression
1 elin2.x . . 3 𝑋 = (𝐵𝐶)
21eleq2i 2818 . 2 (𝐴𝑋𝐴 ∈ (𝐵𝐶))
3 elin 3963 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
42, 3bitri 274 1 (𝐴𝑋 ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394   = wceq 1534  wcel 2099  cin 3946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3465  df-in 3954
This theorem is referenced by:  elin3  4199  opelres  5986  elpredgg  6316  fnres  6678  funfvima  7237  fnwelem  8135  ressuppssdif  8189  fz1isolem  14473  isabl  19776  srhmsubclem1  20649  srhmsubc  20652  isidom  20697  isfld  20712  2idlelb  21236  qus1  21257  qusrhm  21259  lmres  23290  isnvc  24698  cvslvec  25138  cvsclm  25139  iscvs  25140  cvsi  25143  ishl  25376  ply1pid  26205  rplogsum  27551  sltres  27687  iscusgr  29349  isphg  30745  ishlo  30815  hhsscms  31206  mayete3i  31656  isogrp  32939  isofld  33183  bj-elid6  36888  bj-isrvec  37012  caures  37472  iscrngo  37708  fldcrngo  37716  isdmn  37766  isolat  38921  srhmsubcALTV  47736
  Copyright terms: Public domain W3C validator