Theorem elin2 4144

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

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

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 3432  df-in 3897

This theorem is referenced by:  elin3  4147  opelres  5945  elpredgg  6273  fnres  6620  funfvima  7179  fnwelem  8075  ressuppssdif  8129  fz1isolem  14417  isabl  19753  isogrp  20093  srhmsubclem1  20648  srhmsubc  20651  isidom  20696  isfld  20711  isofld  20835  2idlelb  21246  qus1  21267  qusrhm  21269  lmres  23278  isnvc  24673  cvslvec  25105  cvsclm  25106  iscvs  25107  cvsi  25110  ishl  25342  ply1pid  26161  rplogsum  27507  ltsres  27643  iscusgr  29504  isphg  30906  ishlo  30976  hhsscms  31367  mayete3i  31817  bj-elid6  37503  bj-isrvec  37627  caures  38098  iscrngo  38334  fldcrngo  38342  isdmn  38392  isolat  39675  srhmsubcALTV  48816