Theorem elin2 4196

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

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106   ∩ cin 3946

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954

This theorem is referenced by:  elin3  4199  opelres  5985  elpredgg  6310  fnres  6674  funfvima  7228  fnwelem  8113  ressuppssdif  8166  fz1isolem  14418  isabl  19646  isfld  20318  df2idl2  20852  2idlelb  20857  qus1  20864  qusrhm  20866  isidom  20914  lmres  22795  isnvc  24203  cvslvec  24632  cvsclm  24633  iscvs  24634  cvsi  24637  ishl  24870  ply1pid  25688  rplogsum  27019  sltres  27154  iscusgr  28664  isphg  30057  ishlo  30127  hhsscms  30518  mayete3i  30968  isogrp  32207  isofld  32408  bj-elid6  36039  bj-isrvec  36163  caures  36616  iscrngo  36852  fldcrngo  36860  isdmn  36910  isolat  38070  srhmsubclem1  46924  srhmsubc  46927  srhmsubcALTV  46945