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

Theorem elin2 4104
 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 2843 . 2 (𝐴𝑋𝐴 ∈ (𝐵𝐶))
3 elin 3876 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
42, 3bitri 278 1 (𝐴𝑋 ↔ (𝐴𝐵𝐴𝐶))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ∩ cin 3859 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867 This theorem is referenced by:  elin3  4107  opelres  5834  elpredim  6143  elpred  6144  elpredg  6145  fnres  6462  funfvima  6990  fnwelem  7836  ressuppssdif  7865  fz1isolem  13884  isabl  18990  isfld  19592  2idlcpbl  20088  qus1  20089  qusrhm  20091  isidom  20158  lmres  22013  isnvc  23410  cvslvec  23839  cvsclm  23840  iscvs  23841  cvsi  23844  ishl  24075  ply1pid  24892  rplogsum  26223  iscusgr  27320  isphg  28712  ishlo  28782  hhsscms  29173  mayete3i  29623  isogrp  30866  isofld  31039  sltres  33462  bj-elid6  34899  bj-isrvec  35022  caures  35512  iscrngo  35748  fldcrng  35756  isdmn  35806  isolat  36822  srhmsubclem1  45113  srhmsubc  45116  srhmsubcALTV  45134
 Copyright terms: Public domain W3C validator