Theorem elin2 4157

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ∩ cin 3902

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-in 3910

This theorem is referenced by:  elin3  4160  opelres  5952  elpredgg  6280  fnres  6627  funfvima  7186  fnwelem  8083  ressuppssdif  8137  fz1isolem  14396  isabl  19725  isogrp  20065  srhmsubclem1  20622  srhmsubc  20625  isidom  20670  isfld  20685  isofld  20809  2idlelb  21220  qus1  21241  qusrhm  21243  lmres  23256  isnvc  24651  cvslvec  25093  cvsclm  25094  iscvs  25095  cvsi  25098  ishl  25330  ply1pid  26156  rplogsum  27506  ltsres  27642  iscusgr  29503  isphg  30905  ishlo  30975  hhsscms  31366  mayete3i  31816  bj-elid6  37425  bj-isrvec  37549  caures  38011  iscrngo  38247  fldcrngo  38255  isdmn  38305  isolat  39588  srhmsubcALTV  48685