Theorem elin2 4134

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

Syntax hints:   ↔ wb 208   ∧ wa 397   = wceq 1548   ∈ wcel 2121   ∩ cin 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-in 3891

This theorem is referenced by:  elin3  4137  opelres  5943  elpredgg  6268  fnres  6615  funfvima  7177  fnwelem  8073  ressuppssdif  8127  fz1isolem  14418  isabl  19753  isogrp  20093  srhmsubclem1  20652  srhmsubc  20655  isidom  20700  isfld  20715  isofld  20839  2idlelb  21249  qus1  21270  qusrhm  21272  lmres  23286  isnvc  24681  cvslvec  25113  cvsclm  25114  iscvs  25115  cvsi  25118  ishl  25350  ply1pid  26169  rplogsum  27511  ltsres  27646  iscusgr  29507  isphg  30908  ishlo  30978  hhsscms  31369  mayete3i  31819  bj-elid6  37543  bj-isrvec  37667  caures  38140  iscrngo  38376  fldcrngo  38384  isdmn  38434  isolat  39717  srhmsubcALTV  48828