Theorem elin2 4153

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ∩ cin 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-in 3906

This theorem is referenced by:  elin3  4156  opelres  5942  elpredgg  6270  fnres  6617  funfvima  7174  fnwelem  8071  ressuppssdif  8125  fz1isolem  14382  isabl  19711  isogrp  20051  srhmsubclem1  20608  srhmsubc  20611  isidom  20656  isfld  20671  isofld  20795  2idlelb  21206  qus1  21227  qusrhm  21229  lmres  23242  isnvc  24637  cvslvec  25079  cvsclm  25080  iscvs  25081  cvsi  25084  ishl  25316  ply1pid  26142  rplogsum  27492  sltres  27628  iscusgr  29440  isphg  30841  ishlo  30911  hhsscms  31302  mayete3i  31752  bj-elid6  37314  bj-isrvec  37438  caures  37900  iscrngo  38136  fldcrngo  38144  isdmn  38194  isolat  39411  srhmsubcALTV  48513