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

Syntax hints:   ↔ wb 205   ∧ wa 394   = wceq 1534   ∈ wcel 2099   ∩ cin 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3465  df-in 3954

This theorem is referenced by:  elin3  4199  opelres  5986  elpredgg  6316  fnres  6678  funfvima  7237  fnwelem  8135  ressuppssdif  8189  fz1isolem  14473  isabl  19776  srhmsubclem1  20649  srhmsubc  20652  isidom  20697  isfld  20712  2idlelb  21236  qus1  21257  qusrhm  21259  lmres  23290  isnvc  24698  cvslvec  25138  cvsclm  25139  iscvs  25140  cvsi  25143  ishl  25376  ply1pid  26205  rplogsum  27551  sltres  27687  iscusgr  29349  isphg  30745  ishlo  30815  hhsscms  31206  mayete3i  31656  isogrp  32939  isofld  33183  bj-elid6  36888  bj-isrvec  37012  caures  37472  iscrngo  37708  fldcrngo  37716  isdmn  37766  isolat  38921  srhmsubcALTV  47736