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

Theorem elin2 4000
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 2877 . 2 (𝐴𝑋𝐴 ∈ (𝐵𝐶))
3 elin 3995 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
42, 3bitri 266 1 (𝐴𝑋 ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384   = wceq 1637  wcel 2156  cin 3768
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-in 3776
This theorem is referenced by:  elin3  4003  elpredim  5905  elpred  5906  elpredg  5907  fnres  6214  funfvima  6713  fnwelem  7522  ressuppssdif  7546  fz1isolem  13458  isabl  18394  isfld  18956  2idlcpbl  19439  qus1  19440  qusrhm  19442  isidom  19509  lmres  21315  isnvc  22709  cvslvec  23134  cvsclm  23135  iscvs  23136  ishl  23368  ply1pid  24152  rplogsum  25429  iscusgr  26541  isphg  27999  ishlo  28070  hhsscms  28463  mayete3i  28914  isogrp  30026  isofld  30126  sltres  32134  caures  33865  iscrngo  34104  fldcrng  34112  isdmn  34162  opelresALTV  34347  isolat  34990  srhmsubclem1  42638  srhmsubc  42641  srhmsubcALTV  42659
  Copyright terms: Public domain W3C validator