Theorem elin2 4103

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-in 4094

This theorem is used by:  elin3  4106  opelres  5992  elpredgg  6343  fnres  6696  funfvima  7267  fnwelem  8180  ressuppssdif  8240  fz1isolem  14647  isabl  20049  isogrp  20389  srhmsubclem1  20980  srhmsubc  20983  isidom  21027  isfld  21044  isofld  21172  2idlelb  21597  qus1  21619  qusrhm  21621  lmres  23673  isnvc  25069  cvslvec  25501  cvsclm  25502  iscvs  25503  cvsi  25506  ishl  25738  ply1pid  26556  rplogsum  27911  ltsres  28076  iscusgr  30056  isphg  31476  ishlo  31546  hhsscms  31937  mayete3i  32387  fwfffunres  35829  bj-elid6  38359  bj-isrvec  38483  caures  38960  iscrngo  39196  fldcrngo  39204  isdmn  39254  isolat  40535  srhmsubcALTV  49695  isidom2  49772