Theorem elin2 4213

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 2831	. 2 ⊢ (𝐴 ∈ 𝑋 ↔ 𝐴 ∈ (𝐵 ∩ 𝐶))
3		elin 3979	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
4	2, 3	bitri 275	1 ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2106   ∩ cin 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-in 3970

This theorem is referenced by:  elin3  4216  opelres  6006  elpredgg  6336  fnres  6696  funfvima  7250  fnwelem  8155  ressuppssdif  8209  fz1isolem  14497  isabl  19817  srhmsubclem1  20694  srhmsubc  20697  isidom  20742  isfld  20757  2idlelb  21281  qus1  21302  qusrhm  21304  lmres  23324  isnvc  24732  cvslvec  25172  cvsclm  25173  iscvs  25174  cvsi  25177  ishl  25410  ply1pid  26237  rplogsum  27586  sltres  27722  iscusgr  29450  isphg  30846  ishlo  30916  hhsscms  31307  mayete3i  31757  isogrp  33062  isofld  33312  bj-elid6  37153  bj-isrvec  37277  caures  37747  iscrngo  37983  fldcrngo  37991  isdmn  38041  isolat  39194  srhmsubcALTV  48169