Theorem elin2 4131

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894

This theorem is referenced by:  elin3  4134  opelres  5897  elpredgg  6215  fnres  6559  funfvima  7106  fnwelem  7972  ressuppssdif  8001  fz1isolem  14175  isabl  19390  isfld  20000  2idlcpbl  20505  qus1  20506  qusrhm  20508  isidom  20575  lmres  22451  isnvc  23859  cvslvec  24288  cvsclm  24289  iscvs  24290  cvsi  24293  ishl  24526  ply1pid  25344  rplogsum  26675  iscusgr  27785  isphg  29179  ishlo  29249  hhsscms  29640  mayete3i  30090  isogrp  31328  isofld  31501  sltres  33865  bj-elid6  35341  bj-isrvec  35465  caures  35918  iscrngo  36154  fldcrng  36162  isdmn  36212  isolat  37226  srhmsubclem1  45631  srhmsubc  45634  srhmsubcALTV  45652