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

Theorem elin2 4099
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 2874 . 2 (𝐴𝑋𝐴 ∈ (𝐵𝐶))
3 elin 4094 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
42, 3bitri 276 1 (𝐴𝑋 ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396   = wceq 1522  wcel 2081  cin 3862
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-in 3870
This theorem is referenced by:  elin3  4102  opelres  5745  elpredim  6040  elpred  6041  elpredg  6042  fnres  6349  funfvima  6863  fnwelem  7683  ressuppssdif  7707  fz1isolem  13672  isabl  18642  isfld  19206  2idlcpbl  19701  qus1  19702  qusrhm  19704  isidom  19771  lmres  21597  isnvc  22992  cvslvec  23417  cvsclm  23418  iscvs  23419  cvsi  23422  ishl  23653  ply1pid  24461  rplogsum  25790  iscusgr  26888  isphg  28290  ishlo  28360  hhsscms  28751  mayete3i  29201  isogrp  30368  isofld  30534  sltres  32784  caures  34592  iscrngo  34831  fldcrng  34839  isdmn  34889  isolat  35904  srhmsubclem1  43848  srhmsubc  43851  srhmsubcALTV  43869
  Copyright terms: Public domain W3C validator