Theorem elin2 4169

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ∩ cin 3916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-in 3924

This theorem is referenced by:  elin3  4172  opelres  5959  elpredgg  6290  fnres  6648  funfvima  7207  fnwelem  8113  ressuppssdif  8167  fz1isolem  14433  isabl  19721  srhmsubclem1  20593  srhmsubc  20596  isidom  20641  isfld  20656  2idlelb  21170  qus1  21191  qusrhm  21193  lmres  23194  isnvc  24590  cvslvec  25032  cvsclm  25033  iscvs  25034  cvsi  25037  ishl  25269  ply1pid  26095  rplogsum  27445  sltres  27581  iscusgr  29352  isphg  30753  ishlo  30823  hhsscms  31214  mayete3i  31664  isogrp  33023  isofld  33287  bj-elid6  37165  bj-isrvec  37289  caures  37761  iscrngo  37997  fldcrngo  38005  isdmn  38055  isolat  39212  srhmsubcALTV  48317