Theorem elin2 4156

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146   ∩ cin 3905

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913

This theorem is used by:  elin3  4159  opelres  5986  elpredgg  6319  fnres  6666  funfvima  7235  fnwelem  8133  ressuppssdif  8187  fz1isolem  14516  isabl  19898  isogrp  20238  srhmsubclem1  20826  srhmsubc  20829  isidom  20873  isfld  20890  isofld  21017  2idlelb  21442  qus1  21463  qusrhm  21465  lmres  23507  isnvc  24903  cvslvec  25335  cvsclm  25336  iscvs  25337  cvsi  25340  ishl  25572  ply1pid  26391  rplogsum  27742  ltsres  27877  iscusgr  29826  isphg  31240  ishlo  31310  hhsscms  31701  mayete3i  32151  bj-elid6  37871  bj-isrvec  37995  caures  38469  iscrngo  38705  fldcrngo  38713  isdmn  38763  isolat  40044  srhmsubcALTV  49147  isidom2  49166