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

Theorem elin2 4203
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 2833 . 2 (𝐴𝑋𝐴 ∈ (𝐵𝐶))
3 elin 3967 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
42, 3bitri 275 1 (𝐴𝑋 ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1540  wcel 2108  cin 3950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958
This theorem is referenced by:  elin3  4206  opelres  6003  elpredgg  6334  fnres  6695  funfvima  7250  fnwelem  8156  ressuppssdif  8210  fz1isolem  14500  isabl  19802  srhmsubclem1  20677  srhmsubc  20680  isidom  20725  isfld  20740  2idlelb  21263  qus1  21284  qusrhm  21286  lmres  23308  isnvc  24716  cvslvec  25158  cvsclm  25159  iscvs  25160  cvsi  25163  ishl  25396  ply1pid  26222  rplogsum  27571  sltres  27707  iscusgr  29435  isphg  30836  ishlo  30906  hhsscms  31297  mayete3i  31747  isogrp  33079  isofld  33332  bj-elid6  37171  bj-isrvec  37295  caures  37767  iscrngo  38003  fldcrngo  38011  isdmn  38061  isolat  39213  srhmsubcALTV  48241
  Copyright terms: Public domain W3C validator