Theorem elin2 4132

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

Syntax hints:   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890

This theorem is referenced by:  elin3  4135  opelres  5937  elpredgg  6265  fnres  6612  funfvima  7174  fnwelem  8071  ressuppssdif  8125  fz1isolem  14414  isabl  19750  isogrp  20090  srhmsubclem1  20649  srhmsubc  20652  isidom  20697  isfld  20712  isofld  20836  2idlelb  21246  qus1  21267  qusrhm  21269  lmres  23283  isnvc  24678  cvslvec  25110  cvsclm  25111  iscvs  25112  cvsi  25115  ishl  25347  ply1pid  26166  rplogsum  27508  ltsres  27644  iscusgr  29505  isphg  30906  ishlo  30976  hhsscms  31367  mayete3i  31817  bj-elid6  37530  bj-isrvec  37654  caures  38127  iscrngo  38363  fldcrngo  38371  isdmn  38421  isolat  39704  srhmsubcALTV  48816