Theorem elin2 4164

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

Step	Hyp	Ref	Expression
1		elin2.x	. . 3 ⊢ 𝑋 = (𝐵 ∩ 𝐶)
2	1	eleq2i 2861	. 2 ⊢ (𝐴 ∈ 𝑋 ↔ 𝐴 ∈ (𝐵 ∩ 𝐶))
3		elin 3929	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
4	2, 3	bitri 278	1 ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920

This theorem is referenced by:  elin3  4167  opelres  5985  elpredgg  6316  fnres  6663  funfvima  7229  fnwelem  8126  ressuppssdif  8180  fz1isolem  14497  isabl  19853  isogrp  20193  srhmsubclem1  20761  srhmsubc  20764  isidom  20808  isfld  20823  isofld  20944  2idlelb  21362  qus1  21383  qusrhm  21385  lmres  23425  isnvc  24820  cvslvec  25252  cvsclm  25253  iscvs  25254  cvsi  25257  ishl  25489  ply1pid  26308  rplogsum  27656  ltsres  27791  iscusgr  29708  isphg  31109  ishlo  31179  hhsscms  31570  mayete3i  32020  bj-elid6  37701  bj-isrvec  37825  caures  38298  iscrngo  38534  fldcrngo  38542  isdmn  38592  isolat  39875  srhmsubcALTV  48978  isidom2  48997